environment add_namespace(environment const & env, name const & ns) {
    scope_mng_ext ext = get_extension(env);
    if (!ext.m_namespace_set.contains(ns)) {
        ext.m_namespace_set.insert(ns);
        environment r = update(env, ext);
        r = module::add(r, *g_new_namespace_key, [=](environment const &, serializer & s) { s << ns; });
        if (ns.is_atomic())
            return r;
        else
            return add_namespace(r, ns.get_prefix());
    } else {
        return env;
    }
}

environment add_alias(parser & p, environment env, bool composite,
                      name const & full_id, levels const & ctx_levels, buffer<expr> const & ctx_params) {
    name id;
    if (composite)
        id = name(name(full_id.get_prefix().get_string()), full_id.get_string());
    else
        id = name(full_id.get_string());
    if (!empty(ctx_levels) || !ctx_params.empty()) {
        expr r = mk_local_ref(full_id, ctx_levels, ctx_params);
        env = p.add_local_ref(env, id, r);
    }
    if (full_id != id)
        env = add_expr_alias_rec(env, id, full_id);
    return env;
}

json serialize_decl(name const & short_name, name const & long_name, environment const & env, options const & o) {
    declaration const & d = env.get(long_name);
    type_context_old tc(env);
    auto fmter = mk_pretty_formatter_factory()(env, o, tc);
    expr type = d.get_type();
    if (LEAN_COMPLETE_CONSUME_IMPLICIT) {
        while (true) {
            if (!is_pi(type))
                break;
            if (!binding_info(type).is_implicit() && !binding_info(type).is_inst_implicit())
                break;
            std::string q("?");
            q += binding_name(type).to_string();
            expr m = mk_constant(name(q.c_str()));
            type   = instantiate(binding_body(type), m);
        }
    }
    json completion;
    completion["text"] = short_name.to_string();
    interactive_report_type(env, o, type, completion);
    add_source_info(env, long_name, completion);
    if (auto doc = get_doc_string(env, long_name))
        completion["doc"] = *doc;
    return completion;
}

 level collect(level const & l) {
     return replace(l, [&](level const & l) {
             if (is_meta(l)) {
                 name const & id = meta_id(l);
                 if (auto r = m_univ_meta_to_param.find(id)) {
                     return some_level(*r);
                 } else {
                     name n      = m_prefix.append_after(m_next_idx);
                     m_next_idx++;
                     level new_r = mk_param_univ(n);
                     m_univ_meta_to_param.insert(id, new_r);
                     m_univ_meta_to_param_inv.insert(n, l);
                     m_level_params.push_back(n);
                     return some_level(new_r);
                 }
             } else if (is_param(l)) {
                 name const & id = param_id(l);
                 if (!m_found_univ_params.contains(id)) {
                     m_found_univ_params.insert(id);
                     m_level_params.push_back(id);
                 }
             }
             return none_level();
         });
 }

std::string find_file(search_path const & paths, std::string const & base, optional<unsigned> const & rel, name const & fname,
                      std::initializer_list<char const *> const & extensions) {
    if (!rel) {
        return find_file(paths, fname.to_string(get_dir_sep()), extensions);
    } else {
        auto path = base;
        for (unsigned i = 0; i < *rel; i++) {
            path += get_dir_sep();
            path += "..";
        }
        for (auto ext : extensions) {
            if (auto r = check_file(path, fname.to_string(get_dir_sep()), ext))
                return *r;
        }
        throw lean_file_not_found_exception(fname.to_string());
    }
}

std::string find_file(std::string const & base, optional<unsigned> const & rel, name const & fname,
                      std::initializer_list<char const *> const & extensions) {
    if (!rel) {
        return find_file(fname.to_string(g_sep_str.c_str()), extensions);
    } else {
        auto path = base;
        for (unsigned i = 0; i < *rel; i++) {
            path += g_sep;
            path += "..";
        }
        for (auto ext : extensions) {
            if (auto r = check_file(path, fname.to_string(g_sep_str.c_str()), ext))
                return *r;
        }
        throw exception(sstream() << "file '" << fname << "' not found at '" << path << "'");
    }
}

name get_unused_name(name const & prefix, unsigned & idx, buffer<expr> const & locals) {
    while (true) {
        name curr = prefix.append_after(idx);
        idx++;
        if (!uses_name(curr, locals))
            return curr;
    }
}

static name mk_fresh_name(environment const & env, buffer<name> const & names, name const & s) {
    unsigned i = 1;
    name c = s;
    while (true) {
        if (!env.find(c) &&
            std::find(names.begin(), names.end(), c) == names.end())
            return c;
        c = s.append_after(i);
        i++;
    }
}

static unsigned get_precedence(environment const & env, buffer<token_entry> const & new_tokens, name const & token) {
    std::string token_str = token.to_string();
    for (auto const & e : new_tokens) {
        if (e.m_token == token_str)
            return e.m_prec;
    }
    auto prec = get_expr_precedence(get_token_table(env), token_str.c_str());
    if (prec)
        return *prec;
    else
        return 0;
}

void merger::check_name(const std::string& model_name, const name& key,
    const name& value) const {

    if (key.location().original_model_name() != model_name) {
        std::ostringstream s;
        s << "Type does not belong to this model. Model name: '"
          << model_name << "'. Type name: "
          << key.qualified();
        BOOST_LOG_SEV(lg, error) << s.str();
        BOOST_THROW_EXCEPTION(merging_error(s.str()));
    }

    if (key != value) {
        std::ostringstream s;
        s << "Inconsistency between key and value names: "
          << " key: " << key.qualified()
          << " value: " << value.qualified();
        BOOST_LOG_SEV(lg, error) << s.str();
        BOOST_THROW_EXCEPTION(merging_error(s.str()));
    }
}

/// This feature does not define names.
bool
eq_algo::operator()(const name& a, const name& b) const
{
  switch (a.get_kind()) {
    case basic_name_kind:
      return eq_basic_name(cast<basic_name>(a), cast<basic_name>(b));
    case internal_name_kind:
      return eq_internal_name(cast<internal_name>(a), cast<internal_name>(b));
    default:
      break;
  }
  assert(false && "not a core name");
}

/// Hash the name `n` into `h`.
void
hash_algo::operator()(hasher& h, const name& n) const
{
  switch (n.get_kind()) {
    case basic_name_kind:
      return hash(h, cast<basic_name>(n).get_symbol());
    case internal_name_kind:
      return hash(h, cast<internal_name>(n).get_id());
    default:
      break;
  }
  assert(false && "name not a core name");
}

 name mk_name_for(expr const & e) {
     lean_assert(is_nested_declaration(e));
     if (auto n = get_nested_declaration_name(e)) {
         return *n;
     } else {
         name ns  = get_namespace(m_env);
         while (true) {
             name aux = m_dname.append_after(m_idx);
             m_idx++;
             if (!m_env.find(ns + aux))
                 return aux;
         }
     }
 }

void
print_algo::operator()(std::ostream& os, const name& n) const
{
  switch (n.get_kind()) {
    case basic_name_kind:
      os << cast<basic_name>(n).get_symbol().get_spelling();
      return;
    case internal_name_kind:
      os << "<internal>";
      return;
    default:
      break;
  }
  assert(false && "not a core name");
}

    expr visit_cases_on(name const & fn, buffer<expr> & args) {
        name const & I_name = fn.get_prefix();
        if (is_inductive_predicate(env(), I_name))
            throw exception(sstream() << "code generation failed, inductive predicate '" << I_name << "' is not supported");
        bool is_builtin = is_vm_builtin_function(fn);
        buffer<name> cnames;
        get_intro_rule_names(env(), I_name, cnames);
        lean_assert(args.size() >= cnames.size() + 1);
        if (args.size() > cnames.size() + 1)
            distribute_extra_args_over_minors(I_name, cnames, args);
        lean_assert(args.size() == cnames.size() + 1);
        /* Process major premise */
        args[0] = visit(args[0]);
        unsigned num_reachable = 0;
        optional<expr> reachable_case;
        /* Process minor premises */
        for (unsigned i = 0; i < cnames.size(); i++) {
            buffer<bool> rel_fields;
            get_constructor_info(cnames[i], rel_fields);
            auto p = visit_minor_premise(args[i+1], rel_fields);
            expr new_minor = p.first;
            if (i == 0 && has_trivial_structure(I_name, rel_fields)) {
                /* Optimization for an inductive datatype that has a single constructor with only one relevant field */
                return beta_reduce(mk_app(new_minor, args[0]));
            }
            args[i+1] = new_minor;
            if (!p.second) {
                num_reachable++;
                reachable_case = p.first;
            }
        }

        if (num_reachable == 0) {
            return mk_unreachable_expr();
        } else if (num_reachable == 1 && !is_builtin) {
            /* Use _cases.1 */
            return mk_app(mk_cases(1), args[0], *reachable_case);
        } else if (is_builtin) {
            return mk_app(mk_constant(fn), args);
        } else {
            return mk_app(mk_cases(cnames.size()), args);
        }
    }

std::string name_to_file(name const & fname) {
    return fname.to_string(get_dir_sep());
}

 virtual void report(io_state_stream const & ios, json & record) const override {
     record["full-id"] = m_full_id.to_string();
     add_source_info(ios.get_environment(), m_full_id, record);
     if (auto doc = get_doc_string(ios.get_environment(), m_full_id))
         record["doc"] = *doc;
 }