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

Author: <NAME>
*/
#include <algorithm>
#include <string>
#include "util/interrupt.h"
#include "util/list_fn.h"
#include "util/sexpr/option_declarations.h"
#include "kernel/instantiate.h"
#include "kernel/abstract.h"
#include "kernel/replace_fn.h"
#include "kernel/for_each_fn.h"
#include "kernel/inductive/inductive.h"
#include "library/normalize.h"
#include "library/kernel_serializer.h"
#include "library/reducible.h"
#include "library/util.h"
#include "library/match.h"
#include "library/projection.h"
#include "library/local_context.h"
#include "library/unifier.h"
#include "library/constants.h"
#include "library/generic_exception.h"
#include "library/tactic/rewrite_tactic.h"
#include "library/tactic/expr_to_tactic.h"
#include "library/tactic/class_instance_synth.h"

// #define TRACE_MATCH_PLUGIN

#ifndef LEAN_DEFAULT_REWRITER_MAX_ITERATIONS
#define LEAN_DEFAULT_REWRITER_MAX_ITERATIONS 200
#endif

namespace lean {
static name * g_rewriter_max_iterations = nullptr;

unsigned get_rewriter_max_iterations(options const & opts) {
    return opts.get_unsigned(*g_rewriter_max_iterations, LEAN_DEFAULT_REWRITER_MAX_ITERATIONS);
}

class unfold_info {
    list<name> m_names;
    location   m_location;
public:
    unfold_info() {}
    unfold_info(list<name> const & l, location const & loc):m_names(l), m_location(loc) {}
    list<name> const & get_names() const { return m_names; }
    location const & get_location() const { return m_location; }
    friend serializer & operator<<(serializer & s, unfold_info const & e) {
        write_list<name>(s, e.m_names);
        s << e.m_location;
        return s;
    }
    friend deserializer & operator>>(deserializer & d, unfold_info & e) {
        e.m_names = read_list<name>(d);
        d >> e.m_location;
        return d;
    }
};

class reduce_info {
    location  m_location;
public:
    reduce_info() {}
    reduce_info(location const & loc):m_location(loc) {}
    location const & get_location() const { return m_location; }
    friend serializer & operator<<(serializer & s, reduce_info const & e) {
        s << e.m_location;
        return s;
    }
    friend deserializer & operator>>(deserializer & d, reduce_info & e) {
        d >> e.m_location;
        return d;
    }
};

class rewrite_info {
public:
    enum multiplicity { Once, AtMostN, ExactlyN, ZeroOrMore, OneOrMore };
private:
    bool                 m_symm;
    multiplicity         m_multiplicity;
    optional<unsigned>   m_num;
    location             m_location;
    rewrite_info(bool symm, multiplicity m, optional<unsigned> const & n,
                 location const & loc):
        m_symm(symm), m_multiplicity(m), m_num(n), m_location(loc) {}
public:
    rewrite_info():m_symm(false), m_multiplicity(Once) {}
    static rewrite_info mk_once(bool symm, location const & loc) {
        return rewrite_info(symm, Once, optional<unsigned>(), loc);
    }

    static rewrite_info mk_at_most_n(unsigned n, bool symm, location const & loc) {
        return rewrite_info(symm, AtMostN, optional<unsigned>(n), loc);
    }

    static rewrite_info mk_exactly_n(unsigned n, bool symm, location const & loc) {
        return rewrite_info(symm, ExactlyN, optional<unsigned>(n), loc);
    }

    static rewrite_info mk_zero_or_more(bool symm, location const & loc) {
        return rewrite_info(symm, ZeroOrMore, optional<unsigned>(), loc);
    }

    static rewrite_info mk_one_or_more(bool symm, location const & loc) {
        return rewrite_info(symm, OneOrMore, optional<unsigned>(), loc);
    }

    bool symm() const {
        return m_symm;
    }

    multiplicity get_multiplicity() const {
        return m_multiplicity;
    }

    bool has_num() const {
        return multiplicity() == AtMostN || multiplicity() == ExactlyN;
    }
<commit_msg>fix(library/tactic/rewrite_tactic): incorrect assertion<commit_after>/*
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.

Author: <NAME>
*/
#include <algorithm>
#include <string>
#include "util/interrupt.h"
#include "util/list_fn.h"
#include "util/sexpr/option_declarations.h"
#include "kernel/instantiate.h"
#include "kernel/abstract.h"
#include "kernel/replace_fn.h"
#include "kernel/for_each_fn.h"
#include "kernel/inductive/inductive.h"
#include "library/normalize.h"
#include "library/kernel_serializer.h"
#include "library/reducible.h"
#include "library/util.h"
#include "library/match.h"
#include "library/projection.h"
#include "library/local_context.h"
#include "library/unifier.h"
#include "library/constants.h"
#include "library/generic_exception.h"
#include "library/tactic/rewrite_tactic.h"
#include "library/tactic/expr_to_tactic.h"
#include "library/tactic/class_instance_synth.h"

// #define TRACE_MATCH_PLUGIN

#ifndef LEAN_DEFAULT_REWRITER_MAX_ITERATIONS
#define LEAN_DEFAULT_REWRITER_MAX_ITERATIONS 200
#endif

namespace lean {
static name * g_rewriter_max_iterations = nullptr;

unsigned get_rewriter_max_iterations(options const & opts) {
    return opts.get_unsigned(*g_rewriter_max_iterations, LEAN_DEFAULT_REWRITER_MAX_ITERATIONS);
}

class unfold_info {
    list<name> m_names;
    location   m_location;
public:
    unfold_info() {}
    unfold_info(list<name> const & l, location const & loc):m_names(l), m_location(loc) {}
    list<name> const & get_names() const { return m_names; }
    location const & get_location() const { return m_location; }
    friend serializer & operator<<(serializer & s, unfold_info const & e) {
        write_list<name>(s, e.m_names);
        s << e.m_location;
        return s;
    }
    friend deserializer & operator>>(deserializer & d, unfold_info & e) {
        e.m_names = read_list<name>(d);
        d >> e.m_location;
        return d;
    }
};

class reduce_info {
    location  m_location;
public:
    reduce_info() {}
    reduce_info(location const & loc):m_location(loc) {}
    location const & get_location() const { return m_location; }
    friend serializer & operator<<(serializer & s, reduce_info const & e) {
        s << e.m_location;
        return s;
    }
    friend deserializer & operator>>(deserializer & d, reduce_info & e) {
        d >> e.m_location;
        return d;
    }
};

class rewrite_info {
public:
    enum multiplicity { Once, AtMostN, ExactlyN, ZeroOrMore, OneOrMore };
private:
    bool                 m_symm;
    multiplicity         m_multiplicity;
    optional<unsigned>   m_num;
    location             m_location;
    rewrite_info(bool symm, multiplicity m, optional<unsigned> const & n,
                 location const & loc):
        m_symm(symm), m_multiplicity(m), m_num(n), m_location(loc) {}
public:
    rewrite_info():m_symm(false), m_multiplicity(Once) {}
    static rewrite_info mk_once(bool symm, location const & loc) {
        return rewrite_info(symm, Once, optional<unsigned>(), loc);
    }

    static rewrite_info mk_at_most_n(unsigned n, bool symm, location const & loc) {
        return rewrite_info(symm, AtMostN, optional<unsigned>(n), loc);
    }

    static rewrite_info mk_exactly_n(unsigned n, bool symm, location const & loc) {
        return rewrite_info(symm, ExactlyN, optional<unsigned>(n), loc);
    }

    static rewrite_info mk_zero_or_more(bool symm, location const & loc) {
        return rewrite_info(symm, ZeroOrMore, optional<unsigned>(), loc);
    }

    static rewrite_info mk_one_or_more(bool symm, location const & loc) {
        return rewrite_info(symm, OneOrMore, optional<unsigned>(), loc);
    }

    bool symm() const {
        return m_symm;
    }

    multiplicity get_multiplicity() const {
        return m_multiplicity;
    }

    bool has_num() const {
        return get_multiplicity() == AtMostN || get_multiplicity() == ExactlyN;
    }

{'fraction_non_alphanumeric': 0.11390644753476611, 'fraction_numerical': 0.002275600505689001, 'mean_word_length': 3.7286312014345486, 'pattern_counts': {'":': 0, '<': 49, '<?xml version=': 0, '>': 49, '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': '6944479', 'n_tokens_mistral': 2666, 'n_tokens_neox': 2574, 'n_words': 592}