<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 <string>
#include "library/unfold_macros.h"
#include "kernel/type_checker.h"
#include "kernel/inductive/inductive.h"
#include "kernel/standard_kernel.h"
#include "library/module.h"
#include "library/scoped_ext.h"
#include "library/class.h"
#include "library/projection.h"
#include "library/util.h"
#include "library/fingerprint.h"
#include "library/relation_manager.h"
#include "library/inductive_compiler/add_decl.h"
#include "library/inductive_compiler/ginductive.h"
#include "library/inductive_compiler/util.h"
#include "library/vm/vm_nat.h"
#include "library/vm/vm_name.h"
#include "library/vm/vm_option.h"
#include "library/vm/vm_string.h"
#include "library/vm/vm_expr.h"
#include "library/vm/vm_declaration.h"
#include "library/vm/vm_exceptional.h"
#include "library/vm/vm_options.h"
#include "library/vm/vm_list.h"
#include "library/vm/vm_pos_info.h"
#include "library/vm/vm_rb_map.h"
#include "frontends/lean/structure_cmd.h"

namespace lean {
struct vm_environment : public vm_external {
    environment m_val;
    vm_environment(environment const & v):m_val(v) {}
    virtual ~vm_environment() {}
    virtual void dealloc() override { this->~vm_environment(); get_vm_allocator().deallocate(sizeof(vm_environment), this); }
    virtual vm_external * ts_clone(vm_clone_fn const &) override { return new vm_environment(m_val); }
    virtual vm_external * clone(vm_clone_fn const &) override { return new (get_vm_allocator().allocate(sizeof(vm_environment))) vm_environment(m_val); }
};

bool is_env(vm_obj const & o) {
    return is_external(o) && dynamic_cast<vm_environment*>(to_external(o));
}

environment const & to_env(vm_obj const & o) {
    lean_vm_check(dynamic_cast<vm_environment*>(to_external(o)));
    return static_cast<vm_environment*>(to_external(o))->m_val;
}

vm_obj to_obj(environment const & n) {
    return mk_vm_external(new (get_vm_allocator().allocate(sizeof(vm_environment))) vm_environment(n));
}

vm_obj environment_mk_std(vm_obj const & l) {
    return to_obj(mk_environment(force_to_unsigned(l, 0)));
}

vm_obj environment_trust_lvl(vm_obj const & env) {
    return mk_vm_nat(to_env(env).trust_lvl());
}

vm_obj environment_add(vm_obj const & env, vm_obj const & decl) {
    try {
        return mk_vm_exceptional_success(to_obj(module::add(to_env(env), check(to_env(env), to_declaration(decl)))));
    } catch (throwable & ex) {
        return mk_vm_exceptional_exception(ex);
    }
}

vm_obj environment_get(vm_obj const & env, vm_obj const & n) {
    try {
        return mk_vm_exceptional_success(to_obj(to_env(env).get(to_name(n))));
    } catch (throwable & ex) {
        return mk_vm_exceptional_exception(ex);
    }
}

static list<inductive::intro_rule> to_list_intro_rule(vm_obj const & cnstrs) {
    if (is_simple(cnstrs))
        return list<inductive::intro_rule>();
    else
        return list<inductive::intro_rule>(mk_local(to_name(cfield(cfield(cnstrs, 0), 0)),
                                                    to_expr(cfield(cfield(cnstrs, 0), 1))),
                                           to_list_intro_rule(cfield(cnstrs, 1)));
}

vm_obj environment_add_inductive(vm_obj const & env, vm_obj const & n, vm_obj const & ls, vm_obj const & num,
                                 vm_obj const & type, vm_obj const & cnstrs, vm_obj const & is_meta) {
    try {
        environment new_env = module::add_inductive(to_env(env),
                                                    inductive::inductive_decl(to_name(n),
                                                                              to_list_name(ls),
                                                                              force_to_unsigned(num, 0),
                                                                              to_expr(type),
                                                                              to_list_intro_rule(cnstrs)),
                                                    !to_bool(is_meta));
        return mk_vm_exceptional_success(to_obj(new_env));
    } catch (throwable & ex) {
        return mk_vm_exceptional_exception(ex);
    }
}

// meta constant add_ginductive (env : environment) (opt : options)
//   (levels : list name) (params : list expr)
//   (inds : list ((name × expr) × list intro_rule))
//   (is_meta : bool) : exceptional environment
vm_obj environment_add_ginductive(vm_obj const & env, vm_obj const & opts, vm_obj const & ls, vm_obj const & params_,
                                  vm_obj const & inds_, vm_obj const & is_meta) {
    try {
        buffer<expr> params;
        to_buffer_expr(params_, params);
        buffer<name> lp;
        to_buffer_name(ls, lp);
        buffer<expr> inds;
        buffer<buffer<expr>> intro_rules;
        name_map<implicit_infer_kind> implicit_infer_map;

        for (vm_obj const * p = &inds_; !is_simple(*p); p = &cfield(*p, 1)) {
            if (!is_constructor(*p))
                lean_unreachable(); // LCOV_EXCL_LINE
            auto o = cfield(*p, 0);

            inds.push_back(mk_local(to_name(cfield(cfield(o, 0), 0)), to_expr(cfield(cfield(o, 0), 1))));
            intro_rules.emplace_back();
            for (vm_obj const * q = &cfield(o, 1); !is_simple(*q); q = &cfield(*q, 1)) {
                if (!is_constructor(*q))
                    lean_unreachable(); // LCOV_EXCL_LINE
                auto o = cfield(*q, 0);
                auto cname = to_name(cfield(o, 0));
                implicit_infer_map.insert(cname, to_implicit_infer_kind(cfield(o, 2)));
                intro_rules.back().push_back(mk_local(cname, to_expr(cfield(o, 1))));
            }
        }

        if (inds.empty())
            throw exception("cannot declare 0 inductives");

        std::cout << "foo bar\n";
        environment new_env = add_inductive_declaration(
                    to_env(env), to_options(opts), implicit_infer_map,
                    lp, params, inds, intro_rules, !to_bool(is_meta));
        std::cout << "bar foo bar\n";

        return mk_vm_exceptional_success(to_obj(new_env));
    } catch (throwable & ex) {
        return mk_vm_exceptional_exception(ex);
    }
}

vm_obj environment_is_inductive(vm_obj const & env, vm_obj const & n) {
    return mk_vm_bool(static_cast<bool>(inductive::is_inductive_decl(to_env(env), to_name(n))));
}

vm_obj environment_is_constructor(vm_obj const & env, vm_obj const & n) {
    return mk_vm_bool(static_cast<bool>(inductive::is_intro_rule(to_env(env), to_name(n))));
}

vm_obj environment_inductive_type_of(vm_obj const & env, vm_obj const & n) {
    if (auto I = inductive::is_intro_rule(to_env(env), to_name(n)))
        return mk_vm_some(to_obj(*I));
    else
        return mk_vm_none();
}

vm_obj environment_is_recursor(vm_obj const & env, vm_obj const & n) {
    return mk_vm_bool(static_cast<bool>(inductive::is_elim_rule(to_env(env), to_name(n))));
}<commit_msg>fix(vm/vm_environment): remove debug code<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 <string>
#include "library/unfold_macros.h"
#include "kernel/type_checker.h"
#include "kernel/inductive/inductive.h"
#include "kernel/standard_kernel.h"
#include "library/module.h"
#include "library/scoped_ext.h"
#include "library/class.h"
#include "library/projection.h"
#include "library/util.h"
#include "library/fingerprint.h"
#include "library/relation_manager.h"
#include "library/inductive_compiler/add_decl.h"
#include "library/inductive_compiler/ginductive.h"
#include "library/inductive_compiler/util.h"
#include "library/vm/vm_nat.h"
#include "library/vm/vm_name.h"
#include "library/vm/vm_option.h"
#include "library/vm/vm_string.h"
#include "library/vm/vm_expr.h"
#include "library/vm/vm_declaration.h"
#include "library/vm/vm_exceptional.h"
#include "library/vm/vm_options.h"
#include "library/vm/vm_list.h"
#include "library/vm/vm_pos_info.h"
#include "library/vm/vm_rb_map.h"
#include "frontends/lean/structure_cmd.h"

namespace lean {
struct vm_environment : public vm_external {
    environment m_val;
    vm_environment(environment const & v):m_val(v) {}
    virtual ~vm_environment() {}
    virtual void dealloc() override { this->~vm_environment(); get_vm_allocator().deallocate(sizeof(vm_environment), this); }
    virtual vm_external * ts_clone(vm_clone_fn const &) override { return new vm_environment(m_val); }
    virtual vm_external * clone(vm_clone_fn const &) override { return new (get_vm_allocator().allocate(sizeof(vm_environment))) vm_environment(m_val); }
};

bool is_env(vm_obj const & o) {
    return is_external(o) && dynamic_cast<vm_environment*>(to_external(o));
}

environment const & to_env(vm_obj const & o) {
    lean_vm_check(dynamic_cast<vm_environment*>(to_external(o)));
    return static_cast<vm_environment*>(to_external(o))->m_val;
}

vm_obj to_obj(environment const & n) {
    return mk_vm_external(new (get_vm_allocator().allocate(sizeof(vm_environment))) vm_environment(n));
}

vm_obj environment_mk_std(vm_obj const & l) {
    return to_obj(mk_environment(force_to_unsigned(l, 0)));
}

vm_obj environment_trust_lvl(vm_obj const & env) {
    return mk_vm_nat(to_env(env).trust_lvl());
}

vm_obj environment_add(vm_obj const & env, vm_obj const & decl) {
    try {
        return mk_vm_exceptional_success(to_obj(module::add(to_env(env), check(to_env(env), to_declaration(decl)))));
    } catch (throwable & ex) {
        return mk_vm_exceptional_exception(ex);
    }
}

vm_obj environment_get(vm_obj const & env, vm_obj const & n) {
    try {
        return mk_vm_exceptional_success(to_obj(to_env(env).get(to_name(n))));
    } catch (throwable & ex) {
        return mk_vm_exceptional_exception(ex);
    }
}

static list<inductive::intro_rule> to_list_intro_rule(vm_obj const & cnstrs) {
    if (is_simple(cnstrs))
        return list<inductive::intro_rule>();
    else
        return list<inductive::intro_rule>(mk_local(to_name(cfield(cfield(cnstrs, 0), 0)),
                                                    to_expr(cfield(cfield(cnstrs, 0), 1))),
                                           to_list_intro_rule(cfield(cnstrs, 1)));
}

vm_obj environment_add_inductive(vm_obj const & env, vm_obj const & n, vm_obj const & ls, vm_obj const & num,
                                 vm_obj const & type, vm_obj const & cnstrs, vm_obj const & is_meta) {
    try {
        environment new_env = module::add_inductive(to_env(env),
                                                    inductive::inductive_decl(to_name(n),
                                                                              to_list_name(ls),
                                                                              force_to_unsigned(num, 0),
                                                                              to_expr(type),
                                                                              to_list_intro_rule(cnstrs)),
                                                    !to_bool(is_meta));
        return mk_vm_exceptional_success(to_obj(new_env));
    } catch (throwable & ex) {
        return mk_vm_exceptional_exception(ex);
    }
}

// meta constant add_ginductive (env : environment) (opt : options)
//   (levels : list name) (params : list expr)
//   (inds : list ((name × expr) × list intro_rule))
//   (is_meta : bool) : exceptional environment
vm_obj environment_add_ginductive(vm_obj const & env, vm_obj const & opts, vm_obj const & ls, vm_obj const & params_,
                                  vm_obj const & inds_, vm_obj const & is_meta) {
    try {
        buffer<expr> params;
        to_buffer_expr(params_, params);
        buffer<name> lp;
        to_buffer_name(ls, lp);
        buffer<expr> inds;
        buffer<buffer<expr>> intro_rules;
        name_map<implicit_infer_kind> implicit_infer_map;

        for (vm_obj const * p = &inds_; !is_simple(*p); p = &cfield(*p, 1)) {
            if (!is_constructor(*p))
                lean_unreachable(); // LCOV_EXCL_LINE
            auto o = cfield(*p, 0);

            inds.push_back(mk_local(to_name(cfield(cfield(o, 0), 0)), to_expr(cfield(cfield(o, 0), 1))));
            intro_rules.emplace_back();
            for (vm_obj const * q = &cfield(o, 1); !is_simple(*q); q = &cfield(*q, 1)) {
                if (!is_constructor(*q))
                    lean_unreachable(); // LCOV_EXCL_LINE
                auto o = cfield(*q, 0);
                auto cname = to_name(cfield(o, 0));
                implicit_infer_map.insert(cname, to_implicit_infer_kind(cfield(o, 2)));
                intro_rules.back().push_back(mk_local(cname, to_expr(cfield(o, 1))));
            }
        }

        if (inds.empty())
            throw exception("cannot declare 0 inductives");

        environment new_env = add_inductive_declaration(
                    to_env(env), to_options(opts), implicit_infer_map,
                    lp, params, inds, intro_rules, !to_bool(is_meta));

        return mk_vm_exceptional_success(to_obj(new_env));
    } catch (throwable & ex) {
        return mk_vm_exceptional_exception(ex);
    }
}

vm_obj environment_is_inductive(vm_obj const & env, vm_obj const & n) {
    return mk_vm_bool(static_cast<bool>(inductive::is_inductive_decl(to_env(env), to_name(n))));
}

vm_obj environment_is_constructor(vm_obj const & env, vm_obj const & n) {
    return mk_vm_bool(static_cast<bool>(inductive::is_intro_rule(to_env(env), to_name(n))));
}

vm_obj environment_inductive_type_of(vm_obj const & env, vm_obj const & n) {
    if (auto I = inductive::is_intro_rule(to_env(env), to_name(n)))
        return mk_vm_some(to_obj(*I));
    else
        return mk_vm_none();
}

vm_obj environment_is_recursor(vm_obj const & env, vm_obj const & n) {
    return mk_vm_bool(static_cast<bool>(inductive::is_elim_rule(to_env(env), to_name(n))));
}
{'fraction_non_alphanumeric': 0.12216355073497931, 'fraction_numerical': 0.0037105751391465678, 'mean_word_length': 2.8376232201533407, 'pattern_counts': {'":': 0, '<': 41, '<?xml version=': 0, '>': 41, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 44, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '6519722', 'n_tokens_mistral': 4712, 'n_tokens_neox': 4580, 'n_words': 856}