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

Author: <NAME>
*/
#include <deque>
#include "elaborator.h"
#include "metavar.h"
#include "printer.h"
#include "context.h"
#include "builtin.h"
#include "free_vars.h"
#include "for_each.h"
#include "replace.h"
#include "flet.h"
#include "elaborator_exception.h"

namespace lean {
static name g_overload_name(name(name(name(0u), "library"), "overload"));
static expr g_overload = mk_constant(g_overload_name);

bool is_overload_marker(expr const & e) {
    return e == g_overload;
}

expr mk_overload_marker() {
    return g_overload;
}

class elaborator::imp {
    // unification constraint lhs == second
    struct constraint {
        expr     m_lhs;
        expr     m_rhs;
        context  m_ctx;
        expr     m_source;     // auxiliary field used for producing error msgs
        context  m_source_ctx; // auxiliary field used for producing error msgs
        unsigned m_arg_pos;    // auxiliary field used for producing error msgs
        constraint(expr const & lhs, expr const & rhs, context const & ctx, expr const & src, context const & src_ctx, unsigned arg_pos):
            m_lhs(lhs), m_rhs(rhs), m_ctx(ctx), m_source(src), m_source_ctx(src_ctx), m_arg_pos(arg_pos) {}
        constraint(expr const & lhs, expr const & rhs, constraint const & c):
            m_lhs(lhs), m_rhs(rhs), m_ctx(c.m_ctx), m_source(c.m_source), m_source_ctx(c.m_source_ctx), m_arg_pos(c.m_arg_pos) {}
        constraint(expr const & lhs, expr const & rhs, context const & ctx, constraint const & c):
            m_lhs(lhs), m_rhs(rhs), m_ctx(ctx), m_source(c.m_source), m_source_ctx(c.m_source_ctx), m_arg_pos(c.m_arg_pos) {}
    };

    // information associated with the metavariable
    struct metavar_info {
        expr    m_assignment;
        expr    m_type;
        expr    m_mvar;
        context m_ctx;
        bool    m_mark; // for implementing occurs check
        metavar_info() {
            m_mark = false;
        }
    };

    typedef std::deque<constraint>    constraint_queue;
    typedef std::vector<metavar_info> metavars;

    environment const & m_env;
    name_set const *    m_available_defs;
    elaborator const *  m_owner;

    constraint_queue    m_constraints;
    metavars            m_metavars;

    bool                m_add_constraints;

    volatile bool       m_interrupted;

    expr metavar_type(expr const & m) {
        lean_assert(is_metavar(m));
        unsigned midx = metavar_idx(m);
        if (m_metavars[midx].m_type) {
            return m_metavars[midx].m_type;
        } else {
            expr t = mk_metavar();
            m_metavars[midx].m_type = t;
            return t;
        }
    }

    expr lookup(context const & c, unsigned i) {
        auto p = lookup_ext(c, i);
        context_entry const & def = p.first;
        context const & def_c     = p.second;
        lean_assert(length(c) > length(def_c));
        return lift_free_vars_mmv(def.get_domain(), 0, length(c) - length(def_c));
    }

    expr check_pi(expr const & e, context const & ctx, expr const & s, context const & s_ctx) {
        check_interrupted(m_interrupted);
        if (is_pi(e)) {
            return e;
        } else {
            expr r = head_reduce_mmv(e, m_env, m_available_defs);
            if (!is_eqp(r, e)) {
                return check_pi(r, ctx, s, s_ctx);
            } else if (is_var(e)) {
                try {
                    auto p = lookup_ext(ctx, var_idx(e));
                    context_entry const & entry = p.first;
                    context const & entry_ctx   = p.second;
                    if (entry.get_body()) {
                        return lift_free_vars_mmv(check_pi(entry.get_body(), entry_ctx, s, s_ctx), 0, length(ctx) - length(entry_ctx));
                    }
                } catch (exception&) {
                    // this can happen if we access a variable out of scope
                    throw function_expected_exception(m_env, s_ctx, s);
                }
            }
            throw function_expected_exception(m_env, s_ctx, s);
        }
    }

    level check_universe(expr const & e, context const & ctx, expr const & s, context const & s_ctx) {
        check_interrupted(m_interrupted);
        if (is_metavar(e)) {
            // approx: assume it is level 0
            return level();
        } else if (is_type(e)) {
            return ty_level(e);
        } else {
            expr r = head_reduce_mmv(e, m_env, m_available_defs);
            if (!is_eqp(r, e)) {
                return check_universe(r, ctx, s, s_ctx);
            } else if (is_var(e)) {
                try {
                    auto p = lookup_ext(ctx, var_idx(e));
                    context_entry const & entry = p.first;
                    context const & entry_ctx   = p.second;
                    if (entry.get_body()) {
                        return check_universe(entry.get_body(), entry_ctx, s, s_ctx);
                    }<commit_msg>Fix missing case in the elaborator<commit_after>/*
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.

Author: <NAME>
*/
#include <deque>
#include "elaborator.h"
#include "metavar.h"
#include "printer.h"
#include "context.h"
#include "builtin.h"
#include "free_vars.h"
#include "for_each.h"
#include "replace.h"
#include "flet.h"
#include "elaborator_exception.h"

namespace lean {
static name g_overload_name(name(name(name(0u), "library"), "overload"));
static expr g_overload = mk_constant(g_overload_name);

bool is_overload_marker(expr const & e) {
    return e == g_overload;
}

expr mk_overload_marker() {
    return g_overload;
}

class elaborator::imp {
    // unification constraint lhs == second
    struct constraint {
        expr     m_lhs;
        expr     m_rhs;
        context  m_ctx;
        expr     m_source;     // auxiliary field used for producing error msgs
        context  m_source_ctx; // auxiliary field used for producing error msgs
        unsigned m_arg_pos;    // auxiliary field used for producing error msgs
        constraint(expr const & lhs, expr const & rhs, context const & ctx, expr const & src, context const & src_ctx, unsigned arg_pos):
            m_lhs(lhs), m_rhs(rhs), m_ctx(ctx), m_source(src), m_source_ctx(src_ctx), m_arg_pos(arg_pos) {}
        constraint(expr const & lhs, expr const & rhs, constraint const & c):
            m_lhs(lhs), m_rhs(rhs), m_ctx(c.m_ctx), m_source(c.m_source), m_source_ctx(c.m_source_ctx), m_arg_pos(c.m_arg_pos) {}
        constraint(expr const & lhs, expr const & rhs, context const & ctx, constraint const & c):
            m_lhs(lhs), m_rhs(rhs), m_ctx(ctx), m_source(c.m_source), m_source_ctx(c.m_source_ctx), m_arg_pos(c.m_arg_pos) {}
    };

    // information associated with the metavariable
    struct metavar_info {
        expr    m_assignment;
        expr    m_type;
        expr    m_mvar;
        context m_ctx;
        bool    m_mark; // for implementing occurs check
        metavar_info() {
            m_mark = false;
        }
    };

    typedef std::deque<constraint>    constraint_queue;
    typedef std::vector<metavar_info> metavars;

    environment const & m_env;
    name_set const *    m_available_defs;
    elaborator const *  m_owner;

    constraint_queue    m_constraints;
    metavars            m_metavars;

    bool                m_add_constraints;

    volatile bool       m_interrupted;

    expr metavar_type(expr const & m) {
        lean_assert(is_metavar(m));
        unsigned midx = metavar_idx(m);
        if (m_metavars[midx].m_type) {
            return m_metavars[midx].m_type;
        } else {
            expr t = mk_metavar();
            m_metavars[midx].m_type = t;
            return t;
        }
    }

    expr lookup(context const & c, unsigned i) {
        auto p = lookup_ext(c, i);
        context_entry const & def = p.first;
        context const & def_c     = p.second;
        lean_assert(length(c) > length(def_c));
        return lift_free_vars_mmv(def.get_domain(), 0, length(c) - length(def_c));
    }

    expr check_pi(expr const & e, context const & ctx, expr const & s, context const & s_ctx) {
        check_interrupted(m_interrupted);
        if (is_pi(e)) {
            return e;
        } else {
            expr r = head_reduce_mmv(e, m_env, m_available_defs);
            if (!is_eqp(r, e)) {
                return check_pi(r, ctx, s, s_ctx);
            } else if (is_var(e)) {
                try {
                    auto p = lookup_ext(ctx, var_idx(e));
                    context_entry const & entry = p.first;
                    context const & entry_ctx   = p.second;
                    if (entry.get_body()) {
                        return lift_free_vars_mmv(check_pi(entry.get_body(), entry_ctx, s, s_ctx), 0, length(ctx) - length(entry_ctx));
                    }
                } catch (exception&) {
                    // this can happen if we access a variable out of scope
                    throw function_expected_exception(m_env, s_ctx, s);
                }
            }
            throw function_expected_exception(m_env, s_ctx, s);
        }
    }

    level check_universe(expr const & e, context const & ctx, expr const & s, context const & s_ctx) {
        check_interrupted(m_interrupted);
        if (is_metavar(e)) {
            // approx: assume it is level 0
            return level();
        } else if (is_type(e)) {
            return ty_level(e);
        } else if (e == Bool) {
            return level();
        } else {
            expr r = head_reduce_mmv(e, m_env, m_available_defs);
            if (!is_eqp(r, e)) {
                return check_universe(r, ctx, s, s_ctx);
            } else if (is_var(e)) {
                try {
                    auto p = lookup_ext(ctx, var_idx(e));
                    context_entry const & entry = p.first;
                    context const & entry_ctx   = p.second;
                    if (entry.get_body()) {
                        return check_universe(entry.get_body(), entry_ctx, s, s_ctx);
                    }
{'fraction_non_alphanumeric': 0.10341453869484395, 'fraction_numerical': 0.0019567556990509735, 'mean_word_length': 2.05043270665473, 'pattern_counts': {'":': 0, '<': 11, '<?xml version=': 0, '>': 13, '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': '6314255', 'n_tokens_mistral': 3314, 'n_tokens_neox': 3249, 'n_words': 813}