<commit_before>/*
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.

Author: <NAME>
*/
#include <algorithm>
#include "kernel/type_checker.h"
#include "kernel/replace_fn.h"
#include "library/locals.h"
#include "library/placeholder.h"
#include "library/module.h"
#include "library/trace.h"
#include "library/aux_definition.h"
#include "library/unfold_macros.h"
#include "library/replace_visitor_with_tc.h"

namespace lean {
level closure_helper::collect(level const & l) {
    lean_assert(!m_finalized_collection);
    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)) {
                lean_assert(!is_placeholder(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();
        });
}

levels closure_helper::collect(levels const & ls) {
    lean_assert(!m_finalized_collection);
    bool modified = false;
    buffer<level> r;
    for (level const & l : ls) {
        level new_l = collect(l);
        if (new_l != l) modified = true;
        r.push_back(new_l);
    }
    if (!modified)
        return ls;
    else
        return to_list(r);
}

expr closure_helper::collect(expr const & e) {
    lean_assert(!m_finalized_collection);
    return replace(e, [&](expr const & e, unsigned) {
            if (is_metavar(e)) {
                name const & id = mlocal_name(e);
                if (auto r = m_meta_to_param.find(id)) {
                    return some_expr(*r);
                } else {
                    expr type  = m_ctx.infer(e);
                    expr x     = m_ctx.push_local("_x", type);
                    m_meta_to_param.insert(id, x);
                    m_meta_to_param_inv.insert(mlocal_name(x), e);
                    m_params.push_back(x);
                    return some_expr(x);
                }
            } else if (is_local(e)) {
                name const & id = mlocal_name(e);
                if (!m_found_local.contains(id)) {
                    m_found_local.insert(id);
                    m_params.push_back(e);
                }
            } else if (is_sort(e)) {
                return some_expr(update_sort(e, collect(sort_level(e))));
            } else if (is_constant(e)) {
                return some_expr(update_constant(e, collect(const_levels(e))));
            }
            return none_expr();
        });
}

void closure_helper::finalize_collection() {
    lean_assert(!m_finalized_collection);
    name_map<expr> new_types;
    for (unsigned i = 0; i < m_params.size(); i++) {
        expr x = m_params[i];
        expr new_type = collect(zeta_expand(m_ctx.lctx(), m_ctx.instantiate_mvars(m_ctx.infer(x))));
        new_types.insert(mlocal_name(x), new_type);
    }
    local_context const & lctx = m_ctx.lctx();<commit_msg>fix(library/aux_definition): make sure aux_definition level params are sorted<commit_after>/*
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.

Author: <NAME>
*/
#include <algorithm>
#include "kernel/type_checker.h"
#include "kernel/replace_fn.h"
#include "library/locals.h"
#include "library/placeholder.h"
#include "library/module.h"
#include "library/trace.h"
#include "library/aux_definition.h"
#include "library/unfold_macros.h"
#include "library/replace_visitor_with_tc.h"

namespace lean {
level closure_helper::collect(level const & l) {
    lean_assert(!m_finalized_collection);
    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)) {
                lean_assert(!is_placeholder(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();
        });
}

levels closure_helper::collect(levels const & ls) {
    lean_assert(!m_finalized_collection);
    bool modified = false;
    buffer<level> r;
    for (level const & l : ls) {
        level new_l = collect(l);
        if (new_l != l) modified = true;
        r.push_back(new_l);
    }
    if (!modified)
        return ls;
    else
        return to_list(r);
}

expr closure_helper::collect(expr const & e) {
    lean_assert(!m_finalized_collection);
    return replace(e, [&](expr const & e, unsigned) {
            if (is_metavar(e)) {
                name const & id = mlocal_name(e);
                if (auto r = m_meta_to_param.find(id)) {
                    return some_expr(*r);
                } else {
                    expr type  = m_ctx.infer(e);
                    expr x     = m_ctx.push_local("_x", type);
                    m_meta_to_param.insert(id, x);
                    m_meta_to_param_inv.insert(mlocal_name(x), e);
                    m_params.push_back(x);
                    return some_expr(x);
                }
            } else if (is_local(e)) {
                name const & id = mlocal_name(e);
                if (!m_found_local.contains(id)) {
                    m_found_local.insert(id);
                    m_params.push_back(e);
                }
            } else if (is_sort(e)) {
                return some_expr(update_sort(e, collect(sort_level(e))));
            } else if (is_constant(e)) {
                return some_expr(update_constant(e, collect(const_levels(e))));
            }
            return none_expr();
        });
}

void closure_helper::finalize_collection() {
    lean_assert(!m_finalized_collection);
    std::sort(m_level_params.begin(), m_level_params.end());
    name_map<expr> new_types;
    for (unsigned i = 0; i < m_params.size(); i++) {
        expr x = m_params[i];
        expr new_type = collect(zeta_expand(m_ctx.lctx(), m_ctx.instantiate_mvars(m_ctx.infer(x))));
        new_types.insert(mlocal_name(x), new_type);
    }
    local_context const & lctx = m_ctx.lctx();
{'fraction_non_alphanumeric': 0.1172780580935497, 'fraction_numerical': 0.0019091776898949953, 'mean_word_length': 1.881728880157171, 'pattern_counts': {'":': 0, '<': 13, '<?xml version=': 0, '>': 11, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '220640', 'n_tokens_mistral': 2365, 'n_tokens_neox': 2272, 'n_words': 436}