chore(library): remove more dead code
This commit is contained in:
Leonardo de Moura
parent
bbd10b99f7
commit
10b799c341
7 changed files with 3 additions and 537 deletions
|
|
@ -15,14 +15,10 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp
|
|||
fun_info.cpp congr_lemma.cpp defeq_canonizer.cpp scope_pos_info_provider.cpp
|
||||
mpq_macro.cpp arith_instance_manager.cpp replace_visitor_with_tc.cpp
|
||||
aux_definition.cpp inverse.cpp library_system.cpp rfl_lemmas.cpp
|
||||
pattern_attribute.cpp
|
||||
pattern_attribute.cpp choice.cpp locals.cpp
|
||||
|
||||
# Legacy -- The following files will be eventually deleted
|
||||
normalize.cpp justification.cpp constraint.cpp metavar.cpp choice.cpp locals.cpp
|
||||
normalize.cpp justification.cpp constraint.cpp metavar.cpp
|
||||
old_type_context.cpp legacy_type_context.cpp old_type_checker.cpp old_converter.cpp old_default_converter.cpp
|
||||
old_util.cpp old_local_context.cpp choice_iterator.cpp
|
||||
old_tmp_type_context.cpp
|
||||
|
||||
# light_lt_manager.cpp
|
||||
# proof_irrel_expr_manager.cpp
|
||||
old_util.cpp
|
||||
)
|
||||
|
|
|
|||
|
|
@ -1,27 +0,0 @@
|
|||
/*
|
||||
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Leonardo de Moura
|
||||
*/
|
||||
#include "library/choice_iterator.h"
|
||||
|
||||
namespace lean {
|
||||
lazy_list<constraints> choose(std::shared_ptr<choice_iterator> c, bool ignore_failure) {
|
||||
return mk_lazy_list<constraints>([=]() {
|
||||
auto s = c->next();
|
||||
if (s) {
|
||||
return some(mk_pair(*s, choose(c, false)));
|
||||
} else if (ignore_failure) {
|
||||
// return singleton empty list of constraints, and let tactic hints try to instantiate the metavariable.
|
||||
return lazy_list<constraints>::maybe_pair(constraints(), lazy_list<constraints>());
|
||||
} else {
|
||||
return lazy_list<constraints>::maybe_pair();
|
||||
}
|
||||
});
|
||||
}
|
||||
|
||||
lazy_list<constraints> choose(std::shared_ptr<choice_iterator> c) {
|
||||
return choose(c, c->ignore_failure());
|
||||
}
|
||||
}
|
||||
|
|
@ -1,28 +0,0 @@
|
|||
/*
|
||||
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Leonardo de Moura
|
||||
*/
|
||||
#pragma once
|
||||
#include "util/lazy_list.h"
|
||||
#include "library/constraint.h"
|
||||
|
||||
namespace lean {
|
||||
/** \brief Abstract (helper) class for creating lazy_list<constraints> */
|
||||
class choice_iterator {
|
||||
bool m_ignore_failure;
|
||||
public:
|
||||
choice_iterator(bool ignore_failure = false):m_ignore_failure(ignore_failure) {}
|
||||
virtual ~choice_iterator() {}
|
||||
virtual optional<constraints> next() = 0;
|
||||
bool ignore_failure() const { return m_ignore_failure; }
|
||||
};
|
||||
|
||||
/** \brief Convert a choice_iterator into a lazy_list<constraints>
|
||||
The lazy list is generated by invoking the method \c choice_iterator::next.
|
||||
If c->ignore_failure() is true AND \c c does not produce any result,
|
||||
then the singleton lazy_list is produced with an empty set of constraints.
|
||||
*/
|
||||
lazy_list<constraints> choose(std::shared_ptr<choice_iterator> c);
|
||||
}
|
||||
|
|
@ -1,123 +0,0 @@
|
|||
/*
|
||||
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Leonardo de Moura
|
||||
*/
|
||||
#include "util/fresh_name.h"
|
||||
#include "kernel/abstract.h"
|
||||
#include "kernel/replace_fn.h"
|
||||
#include "library/metavar.h"
|
||||
#include "library/old_local_context.h"
|
||||
|
||||
namespace lean {
|
||||
/** \brief Given a list of local constants \c locals
|
||||
(x_n : A_n) ... (x_0 : A_0)
|
||||
and a term \c e
|
||||
t[x_0, ..., x_n]
|
||||
return
|
||||
t[#n, ..., #0]
|
||||
*/
|
||||
expr old_local_context::abstract_locals(expr const & e, list<expr> const & locals) {
|
||||
lean_assert(std::all_of(locals.begin(), locals.end(), [](expr const & e) { return closed(e) && is_local(e); }));
|
||||
if (!has_local(e))
|
||||
return e;
|
||||
return replace(e, [=](expr const & m, unsigned offset) -> optional<expr> {
|
||||
if (!has_local(m))
|
||||
return some_expr(m); // expression m does not contain local constants
|
||||
if (is_local(m)) {
|
||||
unsigned i = 0;
|
||||
for (expr const & l : locals) {
|
||||
if (mlocal_name(l) == mlocal_name(m))
|
||||
return some_expr(copy_tag(m, mk_var(offset + i)));
|
||||
i++;
|
||||
}
|
||||
return none_expr();
|
||||
}
|
||||
return none_expr();
|
||||
});
|
||||
}
|
||||
|
||||
auto old_local_context::to_local_decl(expr const & l, list<expr> const & ctx) -> local_decl {
|
||||
return local_decl(local_pp_name(l), abstract_locals(mlocal_type(l), ctx), local_info(l));
|
||||
}
|
||||
|
||||
old_local_context::old_local_context() {}
|
||||
old_local_context::old_local_context(list<expr> const & ctx) {
|
||||
set_ctx(ctx);
|
||||
}
|
||||
|
||||
void old_local_context::set_ctx(list<expr> const & ctx) {
|
||||
m_ctx = ctx;
|
||||
buffer<local_decl> tmp;
|
||||
list<expr> it = ctx;
|
||||
while (it) {
|
||||
tmp.push_back(to_local_decl(head(it), tail(it)));
|
||||
it = tail(it);
|
||||
}
|
||||
m_ctx_abstracted = to_list(tmp.begin(), tmp.end());
|
||||
}
|
||||
|
||||
expr old_local_context::pi_abstract_context(expr e, tag g) const {
|
||||
e = abstract_locals(e, m_ctx);
|
||||
for (local_decl const & l : m_ctx_abstracted)
|
||||
e = mk_pi(std::get<0>(l), std::get<1>(l), e, std::get<2>(l), g);
|
||||
return e;
|
||||
}
|
||||
|
||||
static expr apply_context_core(expr const & f, list<expr> const & ctx, tag g) {
|
||||
if (ctx)
|
||||
return mk_app(apply_context_core(f, tail(ctx), g), head(ctx), g);
|
||||
else
|
||||
return f;
|
||||
}
|
||||
|
||||
expr old_local_context::apply_context(expr const & f, tag g) const {
|
||||
return apply_context_core(f, m_ctx, g);
|
||||
}
|
||||
|
||||
expr old_local_context::mk_type_metavar(tag g) const {
|
||||
name n = mk_fresh_name();
|
||||
expr s = mk_sort(mk_meta_univ(mk_fresh_name()), g);
|
||||
expr t = pi_abstract_context(s, g);
|
||||
return ::lean::mk_metavar(n, t, g);
|
||||
}
|
||||
|
||||
expr old_local_context::mk_type_meta(tag g) const {
|
||||
return apply_context(mk_type_metavar(g), g);
|
||||
}
|
||||
|
||||
expr old_local_context::mk_metavar(optional<name> const & suffix, optional<expr> const & type, tag g) const {
|
||||
name n = mk_fresh_name();
|
||||
if (suffix)
|
||||
n = n + *suffix;
|
||||
expr r_type = type ? *type : mk_type_meta(g);
|
||||
expr t = pi_abstract_context(r_type, g);
|
||||
return ::lean::mk_metavar(n, t, g);
|
||||
}
|
||||
|
||||
expr old_local_context::mk_meta(optional<name> const & suffix, optional<expr> const & type, tag g) const {
|
||||
expr mvar = mk_metavar(suffix, type, g);
|
||||
expr meta = apply_context(mvar, g);
|
||||
return meta;
|
||||
}
|
||||
|
||||
void old_local_context::add_local(expr const & l) {
|
||||
lean_assert(is_local(l));
|
||||
m_ctx_abstracted = cons(to_local_decl(l, m_ctx), m_ctx_abstracted);
|
||||
m_ctx = cons(l, m_ctx);
|
||||
lean_assert(length(m_ctx) == length(m_ctx_abstracted));
|
||||
}
|
||||
|
||||
list<expr> const & old_local_context::get_data() const {
|
||||
return m_ctx;
|
||||
}
|
||||
|
||||
static list<expr> instantiate_locals(list<expr> const & ls, substitution & s) {
|
||||
return map(ls, [&](expr const & l) { return update_mlocal(l, s.instantiate(mlocal_type(l))); });
|
||||
}
|
||||
|
||||
old_local_context old_local_context::instantiate(substitution s) const {
|
||||
return old_local_context(instantiate_locals(m_ctx, s));
|
||||
}
|
||||
}
|
||||
|
|
@ -1,95 +0,0 @@
|
|||
/*
|
||||
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Leonardo de Moura
|
||||
*/
|
||||
#pragma once
|
||||
#include "util/name_map.h"
|
||||
#include "kernel/expr.h"
|
||||
|
||||
namespace lean {
|
||||
/** \brief Auxiliary data-structure for storing the local context,
|
||||
and creating metavariables in the scope of the local context efficiently
|
||||
*/
|
||||
class old_local_context {
|
||||
list<expr> m_ctx; // current local context: a list of local constants
|
||||
typedef std::tuple<name, expr, binder_info> local_decl;
|
||||
list<local_decl> m_ctx_abstracted; // m_ctx where elements have been abstracted
|
||||
static expr abstract_locals(expr const & e, list<expr> const & locals);
|
||||
// convert a local constant into a local_decl
|
||||
static local_decl to_local_decl(expr const & l, list<expr> const & ctx);
|
||||
public:
|
||||
old_local_context();
|
||||
old_local_context(list<expr> const & ctx);
|
||||
|
||||
void set_ctx(list<expr> const & ctx);
|
||||
|
||||
/** \brief Given <tt>e[l_1, ..., l_n]</tt> and assuming \c m_ctx is
|
||||
<tt>[l_n : A_n[l_1, ..., l_{n-1}], ..., l_1 : A_1 ]</tt>,
|
||||
then the result is
|
||||
<tt>(Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), e[x_1, ... x_n])</tt>.
|
||||
*/
|
||||
expr pi_abstract_context(expr e, tag g) const;
|
||||
|
||||
/** \brief Assuming \c m_ctx is
|
||||
<tt>[l_n : A_n[l_1, ..., l_{n-1}], ..., l_1 : A_1 ]</tt>,
|
||||
return <tt>(f l_1 ... l_n)</tt>.
|
||||
*/
|
||||
expr apply_context(expr const & f, tag g) const;
|
||||
|
||||
/** \brief Assuming \c m_ctx is
|
||||
<tt>[l_n : A_n[l_1, ..., l_{n-1}], ..., l_1 : A_1 ]</tt>,
|
||||
return a fresh metavariable \c ?m with type
|
||||
<tt>(Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), Type.{?u})</tt>,
|
||||
where \c ?u is a fresh universe metavariable.
|
||||
*/
|
||||
expr mk_type_metavar(tag g) const;
|
||||
|
||||
/** \brief Assuming \c m_ctx is
|
||||
<tt>[l_n : A_n[l_1, ..., l_{n-1}], ..., l_1 : A_1 ]</tt>,
|
||||
return <tt>(?m l_1 ... l_n)</tt> where \c ?m is a fresh metavariable with type
|
||||
<tt>(Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), Type.{?u})</tt>,
|
||||
and \c ?u is a fresh universe metavariable.
|
||||
|
||||
\remark The type of the resulting expression is <tt>Type.{?u}</tt>
|
||||
*/
|
||||
expr mk_type_meta(tag g) const;
|
||||
|
||||
/** \brief Given <tt>type[l_1, ..., l_n]</tt> and assuming \c m_ctx is
|
||||
<tt>[l_n : A_n[l_1, ..., l_{n-1}], ..., l_1 : A_1 ]</tt>,
|
||||
then the result is a fresh metavariable \c ?m with type
|
||||
<tt>(Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), type[x_1, ... x_n])</tt>.
|
||||
If <tt>type</tt> is none, then the result is a fresh metavariable \c ?m1 with type
|
||||
<tt>(Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), ?m2 x1 .... xn)</tt>,
|
||||
where ?m2 is another fresh metavariable with type
|
||||
<tt>(Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), Type.{?u})</tt>,
|
||||
and \c ?u is a fresh universe metavariable.
|
||||
|
||||
\remark If \c suffix is not none, then it is appended to the (fresh) metavariable name.
|
||||
*/
|
||||
expr mk_metavar(optional<name> const & suffix, optional<expr> const & type, tag g) const;
|
||||
|
||||
/** \brief Given <tt>type[l_1, ..., l_n]</tt> and assuming \c m_ctx is
|
||||
<tt>[l_n : A_n[l_1, ..., l_{n-1}], ..., l_1 : A_1 ]</tt>,
|
||||
return (?m l_1 ... l_n), where ?m is a fresh metavariable
|
||||
created using \c mk_metavar.
|
||||
|
||||
\see mk_metavar
|
||||
|
||||
\remark If \c suffix is not none, then it is appended to the (fresh) metavariable name.
|
||||
*/
|
||||
expr mk_meta(optional<name> const & suffix, optional<expr> const & type, tag g) const;
|
||||
expr mk_meta(optional<expr> const & type, tag g) const {
|
||||
return mk_meta(optional<name>(), type, g);
|
||||
}
|
||||
|
||||
/** \brief Return context as a list */
|
||||
list<expr> const & get_data() const;
|
||||
|
||||
void add_local(expr const & l);
|
||||
|
||||
/** \brief Instantiate metavariables occurring this local context using \c s, and return updated old_local_context */
|
||||
old_local_context instantiate(substitution s) const;
|
||||
};
|
||||
}
|
||||
|
|
@ -1,144 +0,0 @@
|
|||
/*
|
||||
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Leonardo de Moura
|
||||
*/
|
||||
#include "library/old_tmp_type_context.h"
|
||||
#include "library/idx_metavar.h"
|
||||
|
||||
namespace lean {
|
||||
void old_tmp_type_context::init(environment const & env, reducible_behavior b) {
|
||||
switch (b) {
|
||||
case UnfoldReducible: m_opaque_pred = mk_not_reducible_pred(env); break;
|
||||
case UnfoldSemireducible: m_opaque_pred = mk_irreducible_pred(env); break;
|
||||
}
|
||||
}
|
||||
|
||||
old_tmp_type_context::old_tmp_type_context(environment const & env, options const & o, reducible_behavior b):
|
||||
old_type_context(env, o) {
|
||||
init(env, b);
|
||||
}
|
||||
|
||||
old_tmp_type_context::~old_tmp_type_context() {
|
||||
}
|
||||
|
||||
void old_tmp_type_context::clear() {
|
||||
m_uassignment.clear();
|
||||
m_eassignment.clear();
|
||||
m_trail.clear();
|
||||
m_scopes.clear();
|
||||
clear_infer_cache();
|
||||
}
|
||||
|
||||
void old_tmp_type_context::set_next_uvar_idx(unsigned next_idx) {
|
||||
lean_assert(m_uassignment.empty());
|
||||
lean_assert(m_scopes.empty());
|
||||
m_uassignment.resize(next_idx);
|
||||
}
|
||||
|
||||
void old_tmp_type_context::set_next_mvar_idx(unsigned next_idx) {
|
||||
lean_assert(m_eassignment.empty());
|
||||
lean_assert(m_scopes.empty());
|
||||
m_eassignment.resize(next_idx);
|
||||
}
|
||||
|
||||
bool old_tmp_type_context::is_uvar(level const & l) const {
|
||||
return is_idx_metauniv(l);
|
||||
}
|
||||
|
||||
bool old_tmp_type_context::is_mvar(expr const & e) const {
|
||||
return is_idx_metavar(e);
|
||||
}
|
||||
|
||||
optional<level> old_tmp_type_context::get_assignment(level const & u) const {
|
||||
unsigned idx = to_meta_idx(u);
|
||||
// if the following assetion is violated, we have two options:
|
||||
// 1- We should create the meta-variable using mk_uvar
|
||||
// 2- We create using mk_idx_metauniv, and notify this object using
|
||||
// set_next_uvar_idx
|
||||
lean_assert(idx < m_uassignment.size());
|
||||
return m_uassignment[idx];
|
||||
}
|
||||
|
||||
optional<expr> old_tmp_type_context::get_assignment(expr const & m) const {
|
||||
unsigned idx = to_meta_idx(m);
|
||||
// if the following assetion is violated, we have two options:
|
||||
// 1- We should create the meta-variable using mk_mvar
|
||||
// 2- We create using mk_idx_metavar, and notify this object using
|
||||
// set_next_mvar_idx
|
||||
lean_assert(idx < m_eassignment.size());
|
||||
return m_eassignment[idx];
|
||||
}
|
||||
|
||||
void old_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 old_tmp_type_context::update_assignment(expr const & m, expr const & v) {
|
||||
unsigned idx = to_meta_idx(m);
|
||||
lean_assert(idx < m_eassignment.size()); // see comments above
|
||||
// Remark: type class resolution may update an already assigned meta-variable with a
|
||||
// definitionally equal, but the new assignment is "nicer", i.e., it has not been
|
||||
// accidentally unfolded by the unifier.
|
||||
// We only add the entry to the trail if it was not assigned before.
|
||||
bool was_assigned = static_cast<bool>(m_eassignment[idx]);
|
||||
m_eassignment[idx] = v;
|
||||
if (!m_scopes.empty() && !was_assigned)
|
||||
m_trail.emplace_back(trail_kind::Expr, idx);
|
||||
}
|
||||
|
||||
level old_tmp_type_context::mk_uvar() {
|
||||
unsigned idx = m_uassignment.size();
|
||||
m_uassignment.push_back(none_level());
|
||||
return mk_idx_metauniv(idx);
|
||||
}
|
||||
|
||||
expr old_tmp_type_context::mk_mvar(expr const & type) {
|
||||
unsigned idx = m_eassignment.size();
|
||||
m_eassignment.push_back(none_expr());
|
||||
return mk_idx_metavar(idx, type);
|
||||
}
|
||||
|
||||
void old_tmp_type_context::push_core() {
|
||||
m_scopes.push_back(scope());
|
||||
scope & s = m_scopes.back();
|
||||
s.m_uassignment_sz = m_uassignment.size();
|
||||
s.m_eassignment_sz = m_eassignment.size();
|
||||
s.m_trail_sz = m_trail.size();
|
||||
}
|
||||
|
||||
void old_tmp_type_context::pop_core() {
|
||||
lean_assert(!m_scopes.empty());
|
||||
scope const & s = m_scopes.back();
|
||||
unsigned old_sz = s.m_trail_sz;
|
||||
unsigned i = m_trail.size();
|
||||
while (i > old_sz) {
|
||||
--i;
|
||||
pair<trail_kind, unsigned> const & p = m_trail.back();
|
||||
switch (p.first) {
|
||||
case trail_kind::Level: m_uassignment[p.second] = none_level(); break;
|
||||
case trail_kind::Expr: m_eassignment[p.second] = none_expr(); break;
|
||||
}
|
||||
m_trail.pop_back();
|
||||
}
|
||||
lean_assert(m_trail.size() == old_sz);
|
||||
m_uassignment.resize(s.m_uassignment_sz);
|
||||
m_eassignment.resize(s.m_eassignment_sz);
|
||||
m_scopes.pop_back();
|
||||
}
|
||||
|
||||
unsigned old_tmp_type_context::get_num_check_points() const {
|
||||
return m_scopes.size();
|
||||
}
|
||||
|
||||
void old_tmp_type_context::commit() {
|
||||
lean_assert(!m_scopes.empty());
|
||||
m_scopes.pop_back();
|
||||
}
|
||||
}
|
||||
|
|
@ -1,113 +0,0 @@
|
|||
/*
|
||||
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Leonardo de Moura
|
||||
*/
|
||||
#pragma once
|
||||
#include <vector>
|
||||
#include "library/old_type_context.h"
|
||||
#include "library/reducible.h"
|
||||
|
||||
namespace lean {
|
||||
/** \brief Type context for solving matching and simple unification problems.
|
||||
It only supports meta-variables created with the module idx_metavar.h.
|
||||
Internally, it stores the meta-variable assignments in an array.
|
||||
So, it is assuming the metavariables have small indices.
|
||||
|
||||
The assignment and backtracking stack can be reset using the clear method.
|
||||
|
||||
\remark By default, this object assumes that non-reducible constants are opaque.
|
||||
We can change that by providing a different reducible_behavior value when
|
||||
creating the object.
|
||||
|
||||
\remark The default implementations for infer_local(e) and
|
||||
infer_metavar(e) just return mlocal_type(e). They must be
|
||||
redefined if we want to use this class in modules that store the type
|
||||
of local constants and meta-variables in a different place.
|
||||
|
||||
\remark The local context is set using the method set_context from type_context.
|
||||
*/
|
||||
class old_tmp_type_context : public old_type_context {
|
||||
name_predicate m_opaque_pred;
|
||||
std::vector<optional<level>> m_uassignment;
|
||||
std::vector<optional<expr>> m_eassignment;
|
||||
enum class trail_kind { Level, Expr };
|
||||
std::vector<pair<trail_kind, unsigned>> m_trail; // undo stack
|
||||
struct scope {
|
||||
unsigned m_old_next_local_idx;
|
||||
unsigned m_uassignment_sz;
|
||||
unsigned m_eassignment_sz;
|
||||
unsigned m_trail_sz;
|
||||
};
|
||||
std::vector<scope> m_scopes;
|
||||
void init(environment const & env, reducible_behavior b);
|
||||
public:
|
||||
old_tmp_type_context(environment const & env, options const & o, reducible_behavior b = UnfoldReducible);
|
||||
virtual ~old_tmp_type_context();
|
||||
|
||||
/** \brief Reset the state: backtracking stack, indices and assignment. */
|
||||
void clear();
|
||||
|
||||
/** \remark The following methods are useful when indexed meta-variables have been created outside
|
||||
of this module.
|
||||
\pre This method should only be invoked if not meta-variable has been created.
|
||||
Use the method clear() to ensure this condition holds */
|
||||
void set_next_uvar_idx(unsigned next_idx);
|
||||
|
||||
/** \remark The following methods are useful when indexed meta-variables have been created outside
|
||||
of this module.
|
||||
\pre This method should only be invoked if not meta-variable has been created.
|
||||
Use the method clear() to ensure this condition holds */
|
||||
void set_next_mvar_idx(unsigned next_idx);
|
||||
|
||||
virtual bool is_extra_opaque(name const & n) const { return m_opaque_pred(n); }
|
||||
virtual bool is_uvar(level const & l) const;
|
||||
virtual bool is_mvar(expr const & e) const;
|
||||
virtual optional<level> get_assignment(level const & u) const;
|
||||
virtual optional<expr> get_assignment(expr const & m) const;
|
||||
virtual void update_assignment(level const & u, level const & v);
|
||||
virtual void update_assignment(expr const & m, expr const & v);
|
||||
|
||||
virtual expr infer_local(expr const & e) const { return mlocal_type(e); }
|
||||
virtual expr infer_metavar(expr const & e) const { return mlocal_type(e); }
|
||||
|
||||
virtual level mk_uvar();
|
||||
virtual expr mk_mvar(expr const &);
|
||||
|
||||
virtual void push_core();
|
||||
virtual void pop_core();
|
||||
virtual unsigned get_num_check_points() const;
|
||||
virtual void commit();
|
||||
|
||||
bool is_uvar_assigned(unsigned idx) const {
|
||||
lean_assert(idx < m_uassignment.size());
|
||||
return static_cast<bool>(m_uassignment[idx]);
|
||||
}
|
||||
|
||||
bool is_mvar_assigned(unsigned idx) const {
|
||||
lean_assert(idx < m_eassignment.size());
|
||||
return static_cast<bool>(m_eassignment[idx]);
|
||||
}
|
||||
};
|
||||
|
||||
class old_tmp_type_context_pool {
|
||||
public:
|
||||
virtual old_tmp_type_context * mk_old_tmp_type_context() =0;
|
||||
virtual void recycle_old_tmp_type_context(old_tmp_type_context * tmp_tctx) =0;
|
||||
|
||||
virtual ~old_tmp_type_context_pool() {}
|
||||
};
|
||||
|
||||
class default_old_tmp_type_context_pool : public old_tmp_type_context_pool {
|
||||
environment m_env;
|
||||
options m_options;
|
||||
public:
|
||||
default_old_tmp_type_context_pool(environment const & env, options const & o):
|
||||
m_env(env), m_options(o) {}
|
||||
|
||||
virtual old_tmp_type_context * mk_old_tmp_type_context() override { return new old_tmp_type_context(m_env, m_options); }
|
||||
virtual void recycle_old_tmp_type_context(old_tmp_type_context * tmp_tctx) override { delete tmp_tctx; }
|
||||
};
|
||||
|
||||
}
|
||||
Loading…
Add table
Reference in a new issue