template <typename T, typename X>    void static_matrix<T, X>::check_consistency() {
    std::unordered_map<std::pair<unsigned, unsigned>, T> by_rows;
    for (int i = 0; i < m_rows.size(); i++){
        for (auto & t : m_rows[i]) {
            pair<unsigned, unsigned> p(i, t.m_j);
            lean_assert(by_rows.find(p) == by_rows.end());
            by_rows[p] = t.get_val();
        }
    }
    std::unordered_map<pair<unsigned, unsigned>, T> by_cols;
    for (int i = 0; i < m_columns.size(); i++){
        for (auto & t : m_columns[i]) {
            pair<unsigned, unsigned> p(t.m_i, i);
            lean_assert(by_cols.find(p) == by_cols.end());
            by_cols[p] = get_value_of_column_cell(t);
        }
    }
    lean_assert(by_rows.size() == by_cols.size());

    for (auto & t : by_rows) {
        auto ic = by_cols.find(t.first);
        if (ic == by_cols.end()){
            std::cout << "rows have pair (" << t.first.first <<"," << t.first.second
                      << "), but columns don't " << std::endl;
        }
        lean_assert(ic != by_cols.end());
        lean_assert(t.second == ic->second);
    }
}

// Read until the end_str is found, store all characters (not including end_str) in m_buffer.
// Throw a parser exception error_msg if end of file is found before end_str.
void scanner::read_until(char const * end_str, char const * error_msg) {
    lean_assert(end_str);
    lean_assert(end_str[0]);
    m_buffer.clear();
    while (true) {
        check_not_eof(error_msg);
        char c = curr_next();
        if (c == end_str[0]) {
            m_aux_buffer.clear();
            m_aux_buffer += c;
            unsigned i = 1;
            while (true) {
                if (!end_str[i])
                    return;
                check_not_eof(error_msg);
                c = curr_next();
                if (c != end_str[i]) {
                    m_buffer += m_aux_buffer;
                    break;
                }
                i++;
            }
        } else {
            m_buffer += c;
        }
    }
}

 expr visit_projection(name const & fn, buffer<expr> const & args) {
     projection_info const & info = *get_projection_info(env(), fn);
     expr major = visit(args[info.m_nparams]);
     buffer<bool> rel_fields;
     name I_name = *inductive::is_intro_rule(env(), info.m_constructor);
     get_constructor_info(info.m_constructor, rel_fields);
     lean_assert(info.m_i < rel_fields.size());
     lean_assert(rel_fields[info.m_i]); /* We already erased irrelevant information */
     /* Adjust projection index by ignoring irrelevant fields */
     unsigned j = 0;
     for (unsigned i = 0; i < info.m_i; i++) {
         if (rel_fields[i])
             j++;
     }
     expr r;
     if (has_trivial_structure(I_name, rel_fields)) {
         lean_assert(j == 0);
         r = major;
     } else {
         r = mk_app(mk_proj(j), major);
     }
     /* Add additional arguments */
     for (unsigned i = info.m_nparams + 1; i < args.size(); i++)
         r = mk_app(r, visit(args[i]));
     return r;
 }

coercion_elaborator::coercion_elaborator(coercion_info_manager & info, expr const & arg,
                                         list<constraints> const & choices, list<expr> const & coes,
                                         bool use_id):
    m_info(info), m_arg(arg), m_id(use_id), m_choices(choices), m_coercions(coes) {
    lean_assert(!use_id || length(m_coercions) + 1 == length(m_choices));
    lean_assert(use_id  || length(m_coercions)     == length(m_choices));
}

void get_rec_args(environment const & env, name const & n, buffer<buffer<bool>> & r) {
    lean_assert(inductive::is_inductive_decl(env, n));
    type_checker tc(env);
    name_generator ngen;
    declaration ind_decl   = env.get(n);
    declaration rec_decl   = env.get(inductive::get_elim_name(n));
    unsigned nparams       = *inductive::get_num_params(env, n);
    unsigned nminors       = *inductive::get_num_minor_premises(env, n);
    unsigned ntypeformers  = *inductive::get_num_type_formers(env, n);
    buffer<expr> rec_args;
    to_telescope(ngen, rec_decl.get_type(), rec_args);
    buffer<name> typeformer_names;
    for (unsigned i = nparams; i < nparams + ntypeformers; i++) {
        typeformer_names.push_back(mlocal_name(rec_args[i]));
    }
    lean_assert(typeformer_names.size() == ntypeformers);
    r.clear();
    // add minor premises
    for (unsigned i = nparams + ntypeformers; i < nparams + ntypeformers + nminors; i++) {
        r.push_back(buffer<bool>());
        buffer<bool> & bv = r.back();
        expr minor_type = mlocal_type(rec_args[i]);
        buffer<expr> minor_args;
        to_telescope(ngen, minor_type, minor_args);
        for (expr & minor_arg : minor_args) {
            buffer<expr> minor_arg_args;
            expr minor_arg_type = to_telescope(tc, mlocal_type(minor_arg), minor_arg_args);
            bv.push_back(is_typeformer_app(typeformer_names, minor_arg_type));
        }
    }
}

void tmp_type_context::update_assignment(level const & u, level const & v) {
    unsigned idx = to_meta_idx(u);
    lean_assert(idx < m_uassignment.size()); // see comments above
    lean_assert(!m_uassignment[idx]);
    m_uassignment[idx] = v;
    if (!m_scopes.empty())
        m_trail.emplace_back(trail_kind::Level, idx);
}

void lar_solver::solve_with_core_solver() {
    m_mpq_lar_core_solver.solve();
    m_status = m_mpq_lar_core_solver.m_status;
    lean_assert(m_status != OPTIMAL  || all_constraints_hold());
#ifdef LEAN_DEBUG
    lean_assert(!settings().row_feasibility || m_status != INFEASIBLE || the_evidence_is_correct());
#endif
}

void lar_solver::fill_row_of_A(static_matrix<U, V> & A, unsigned i, canonic_left_side * ls) {
    for (auto & t : ls->m_coeffs) {
        var_index vi = t.second;
        unsigned column = get_column_index_from_var_index(vi);
        lean_assert(is_valid(column));
        A.set(i, column, convert_struct<U, mpq>::convert(t.first));
    }
    unsigned additional_column = get_column_index_from_var_index(ls->m_additional_var_index);
    lean_assert(is_valid(additional_column));
    A.set(i, additional_column, - one_of_type<U>());
}

void lar_solver::prepare_core_solver_fields(static_matrix<U, V> & A, std::vector<V> & x,
                                            std::vector<V> & low_bound,
                                            std::vector<V> & upper_bound) {
    create_matrix_A(A);
    fill_bounds_for_core_solver(low_bound, upper_bound);
    if (m_status == INFEASIBLE) {
        lean_assert(false); // not implemented
    }
    resize_and_init_x_with_zeros(x, A.column_count());
    lean_assert(m_lar_core_solver_params.m_basis.size() == A.row_count());
}

 edge(expr const & e, bool fn) {
     m_fn = fn;
     lean_assert(is_constant(e) || is_local(e));
     if (is_constant(e)) {
         m_kind = edge_kind::Constant;
         m_name = const_name(e);
     } else {
         lean_assert(is_local(e));
         m_kind = edge_kind::Local;
         m_name = mlocal_name(e);
     }
 }

template <typename T, typename X>    unsigned static_matrix<T, X>::lowest_row_in_column(unsigned col) {
    lean_assert(col < column_count());
    column_strip & colstrip = m_columns[col];
    lean_assert(colstrip.size() > 0);
    unsigned ret = 0;
    for (auto & t : colstrip) {
        if (t.m_i > ret) {
            ret = t.m_i;
        }
    }
    return ret;
}

void lar_solver::fill_bounds_for_core_solver(std::vector<V> & lb, std::vector<V> & ub) {
    unsigned n = static_cast<unsigned>(m_map_from_var_index_to_column_info_with_cls.size()); // this is the number of columns
    lb.resize(n);
    ub.resize(n);
    for (auto t : m_set_of_canonic_left_sides) {
        auto & ci = get_column_info_from_var_index(t->m_additional_var_index);
        unsigned j = ci.get_column_index();
        lean_assert(is_valid(j));
        lean_assert(j < n);
        if (ci.low_bound_is_set())
            lb[j] = conversion_helper<V>::get_low_bound(ci);
        if (ci.upper_bound_is_set())
            ub[j] = conversion_helper<V>::get_upper_bound(ci);
    }
}

expr dsimplify_core_fn::visit_app(expr const & e) {
    buffer<expr> args;
    bool modified = false;
    expr f        = get_app_args(e, args);
    unsigned i    = 0;
    if (!m_cfg.m_canonize_instances) {
        fun_info info = get_fun_info(m_ctx, f, args.size());
        for (param_info const & pinfo : info.get_params_info()) {
            lean_assert(i < args.size());
            expr new_a;
            if (pinfo.is_inst_implicit()) {
                new_a = m_defeq_canonizer.canonize(args[i], m_need_restart);
            } else {
                new_a = visit(args[i]);
            }
            if (new_a != args[i])
                modified = true;
            args[i] = new_a;
            i++;
        }
    }
    for (; i < args.size(); i++) {
        expr new_a = visit(args[i]);
        if (new_a != args[i])
            modified = true;
        args[i] = new_a;
    }
    if (modified)
        return mk_app(f, args);
    else
        return e;
}

void get_structure_instance_info(expr const & e,
                                 name & struct_name,
                                 optional<expr> & source,
                                 buffer<name> & field_names,
                                 buffer<expr> & field_values) {
    lean_assert(is_structure_instance(e));
    struct_name = static_cast<structure_instance_macro_cell const*>(macro_def(e).raw())->get_struct();
    list<name> const & fns = static_cast<structure_instance_macro_cell const*>(macro_def(e).raw())->get_field_names();
    to_buffer(fns, field_names);
    unsigned num_fields = field_names.size();
    lean_assert(macro_num_args(e) == num_fields || macro_num_args(e) == num_fields+1);
    if (num_fields < macro_num_args(e))
        source = macro_arg(e, num_fields);
    for (unsigned i = 0; i < num_fields; i++)
        field_values.push_back(macro_arg(e, i));
}

expr replace_visitor::visit_let(expr const & e) {
    lean_assert(is_let(e));
    expr new_t = visit(let_type(e));
    expr new_v = visit(let_value(e));
    expr new_b = visit(let_body(e));
    return update_let(e, new_t, new_v, new_b);
}

void display_decimal(std::ostream & out, mpq const & a, unsigned prec) {
    mpz n1, d1, v1;
    numerator(n1, a);
    denominator(d1, a);
    if (a.is_neg()) {
        out << "-";
        n1.neg();
    }
    v1 = n1 / d1;
    out << v1;
    n1 = rem(n1, d1);
    if (n1.is_zero())
        return;
    out << ".";
    for (unsigned i = 0; i < prec; i++) {
        n1 *= 10;
        v1 = n1 / d1;
        lean_assert(v1 < 10);
        out << v1;
        n1 = rem(n1, d1);
        if (n1.is_zero())
            return;
    }
    out << "?";
}

void expr_cell::dealloc() {
    try {
        del_buffer todo;
        todo.push_back(this);
        while (!todo.empty()) {
            expr_cell * it = todo.back();
            todo.pop_back();
            lean_assert(it->get_rc() == 0);
            switch (it->kind()) {
            case expr_kind::Var:        static_cast<expr_var*>(it)->dealloc(); break;
            case expr_kind::Macro:      static_cast<expr_macro*>(it)->dealloc(todo); break;
            case expr_kind::Meta:       static_cast<expr_mlocal*>(it)->dealloc(todo); break;
            case expr_kind::Local:      static_cast<expr_local*>(it)->dealloc(todo); break;
            case expr_kind::Constant:   static_cast<expr_const*>(it)->dealloc(); break;
            case expr_kind::Sort:       static_cast<expr_sort*>(it)->dealloc(); break;
            case expr_kind::App:        static_cast<expr_app*>(it)->dealloc(todo); break;
            case expr_kind::Lambda:
            case expr_kind::Pi:         static_cast<expr_binding*>(it)->dealloc(todo); break;
            case expr_kind::Let:        static_cast<expr_let*>(it)->dealloc(todo); break;
           }
        }
    } catch (std::bad_alloc&) {
        // We need this catch, because push_back may fail when expanding the buffer.
        // In this case, we avoid the crash, and "accept" the memory leak.
    }
}

void row_eta_matrix<T, X>::apply_from_right(indexed_vector<T> & w) {
    T w_row = w[m_row];
    if (numeric_traits<T>::is_zero(w_row)) return;
#ifdef LEAN_DEBUG
    //        dense_matrix<T> deb(*this);
    // auto clone_w = clone_vector<T>(w.m_data, m_dimension);
    // deb.apply_from_right(clone_w);
#endif
    for (auto & it : m_row_vector.m_data) {
        T old_val = w[it.first];
        T v = w[it.index()] += w_row * it.second;
        if (numeric_traits<T>::is_zero(old_val)) {
            w.m_index.push_back(it.index());
        } else if (numeric_traits<T>::is_zero(v)) { // it is a very rare case
            auto w_it = std::find(w.m_index.begin(), w.m_index.end(), it.index());
            lean_assert(w_it != w.m_index.end());
            w.m_index.erase(w_it);
        }
    }
#ifdef LEAN_DEBUG
    // lean_assert(vectors_are_equal<T>(clone_w, w.m_data, m_dimension));
    // for (unsigned i = 0; i < m_dimension; i++) {
    //     if (!numeric_traits<T>::is_zero(w.m_data[i])) {
    //         lean_assert(std::find(w.m_index.begin(), w.m_index.end(), i) != w.m_index.end());
    //     }
    // }
    // delete clone_w;
#endif
}