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

Author: <NAME>
*/
#include "util/sstream.h"
#include "library/choice.h"
#include "library/kernel_bindings.h"

namespace lean {
static name g_choice_name("choice");
[[ noreturn ]] static void throw_ex() { throw exception("unexpected occurrence of 'choice' expression"); }

// We encode a 'choice' expression using a macro.
// This is a trick to avoid creating a new kind of expression.
// 'Choice' expressions are temporary objects used by the elaborator,
// and have no semantic significance.
class choice_macro_cell : public macro_definition_cell {
public:
    virtual name get_name() const { return g_choice_name; }
    // Choice expressions must be replaced with metavariables before invoking the type checker.
    // Choice expressions cannot be exported. They are transient/auxiliary objects.
    virtual expr get_type(expr const &, expr const *, extension_context &) const { throw_ex(); }
    virtual optional<expr> expand(expr const &, extension_context &) const { throw_ex(); }
    virtual void write(serializer &) const { throw_ex(); }
};

static macro_definition g_choice(new choice_macro_cell());
expr mk_choice(unsigned num_es, expr const * es) {
    lean_assert(num_es > 0);
    if (num_es == 1)
        return es[0];
    else
        return mk_macro(g_choice, num_es, es);
}

bool is_choice(expr const & e) {
    return is_macro(e) && macro_def(e) == g_choice;
}

unsigned get_num_choices(expr const & e) {
    lean_assert(is_choice(e));
    return macro_num_args(e);
}

expr const & get_choice(expr const & e, unsigned i) {
    lean_assert(is_choice(e));
    return macro_arg(e, i);
}

static int mk_choice(lua_State * L) {
    check_atleast_num_args(L, 1);
    int nargs = lua_gettop(L);<commit_msg>fix(library/choice): we should be able to store 'choice' operators in .olean files, this can happen because of notation decls<commit_after>/*
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.

Author: <NAME>
*/
#include "util/sstream.h"
#include "library/choice.h"
#include "library/kernel_bindings.h"
#include "library/kernel_serializer.h"

namespace lean {
static name g_choice_name("choice");
static std::string g_choice_opcode("Choice");
[[ noreturn ]] static void throw_ex() { throw exception("unexpected occurrence of 'choice' expression");
}

// We encode a 'choice' expression using a macro.
// This is a trick to avoid creating a new kind of expression.
// 'Choice' expressions are temporary objects used by the elaborator,
// and have no semantic significance.
class choice_macro_cell : public macro_definition_cell {
public:
    virtual name get_name() const { return g_choice_name; }
    // Choice expressions must be replaced with metavariables before invoking the type checker.
    // Choice expressions cannot be exported. They are transient/auxiliary objects.
    virtual expr get_type(expr const &, expr const *, extension_context &) const { throw_ex(); }
    virtual optional<expr> expand(expr const &, extension_context &) const { throw_ex(); }
    virtual void write(serializer & s) const {
        // we should be able to write choice expressions because of notation declarations
        s.write_string(g_choice_opcode);
    }
};

static macro_definition g_choice(new choice_macro_cell());
expr mk_choice(unsigned num_es, expr const * es) {
    lean_assert(num_es > 0);
    if (num_es == 1)
        return es[0];
    else
        return mk_macro(g_choice, num_es, es);
}

static register_macro_deserializer_fn
choice_macro_des_fn(g_choice_opcode, [](deserializer &, unsigned num, expr const * args) { return mk_choice(num, args); });

bool is_choice(expr const & e) {
    return is_macro(e) && macro_def(e) == g_choice;
}

unsigned get_num_choices(expr const & e) {
    lean_assert(is_choice(e));
    return macro_num_args(e);
}

expr const & get_choice(expr const & e, unsigned i) {
    lean_assert(is_choice(e));
    return macro_arg(e, i);
}

static int mk_choice(lua_State * L) {
    check_atleast_num_args(L, 1);
    int nargs = lua_gettop(L);
{'fraction_non_alphanumeric': 0.10462633451957296, 'fraction_numerical': 0.004744958481613286, 'mean_word_length': 4.336708860759494, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 9, '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': '3357694', 'n_tokens_mistral': 1314, 'n_tokens_neox': 1281, 'n_words': 423}