chore(library/tc_multigraph): remove dead code
This commit is contained in:
parent
d44d576194
commit
765865ed41
3 changed files with 0 additions and 135 deletions
|
@ -40,7 +40,6 @@ Author: Leonardo de Moura
|
|||
#include "library/user_recursors.h"
|
||||
#include "library/class_instance_synth.h"
|
||||
#include "library/composition_manager.h"
|
||||
#include "library/tc_multigraph.h"
|
||||
|
||||
namespace lean {
|
||||
void initialize_library_module() {
|
||||
|
@ -80,11 +79,9 @@ void initialize_library_module() {
|
|||
initialize_user_recursors();
|
||||
initialize_class_instance_elaborator();
|
||||
initialize_composition_manager();
|
||||
initialize_tc_multigraph();
|
||||
}
|
||||
|
||||
void finalize_library_module() {
|
||||
finalize_tc_multigraph();
|
||||
finalize_composition_manager();
|
||||
finalize_class_instance_elaborator();
|
||||
finalize_user_recursors();
|
||||
|
|
|
@ -11,8 +11,6 @@ Author: Leonardo de Moura
|
|||
#include "library/util.h"
|
||||
|
||||
namespace lean {
|
||||
static name * g_fun_sink = nullptr;
|
||||
static name * g_sort_sink = nullptr;
|
||||
struct add_edge_fn {
|
||||
environment m_env;
|
||||
type_checker_ptr m_tc;
|
||||
|
@ -198,125 +196,4 @@ list<name> tc_multigraph::get_predecessors(name const & c) const {
|
|||
else
|
||||
return list<name>();
|
||||
}
|
||||
|
||||
// TODO(Leo): move to coercion module
|
||||
|
||||
/** \brief Return true iff args contains Var(0), Var(1), ..., Var(args.size() - 1) */
|
||||
static bool check_var_args(buffer<expr> const & args) {
|
||||
buffer<bool> found;
|
||||
found.resize(args.size(), false);
|
||||
for (unsigned i = 0; i < args.size(); i++) {
|
||||
if (!is_var(args[i]))
|
||||
return false;
|
||||
unsigned idx = var_idx(args[i]);
|
||||
if (idx >= args.size() || found[idx])
|
||||
return false;
|
||||
found[idx] = true;
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
/** \brief Return true iff param_id(levels[i]) == level_params[i] */
|
||||
static bool check_levels(levels ls, level_param_names ps) {
|
||||
while (!is_nil(ls) && !is_nil(ps)) {
|
||||
if (!is_param(head(ls)))
|
||||
return false;
|
||||
if (param_id(head(ls)) != head(ps))
|
||||
return false;
|
||||
ls = tail(ls);
|
||||
ps = tail(ps);
|
||||
}
|
||||
return is_nil(ls) && is_nil(ps);
|
||||
}
|
||||
|
||||
static void throw_ex(name const & k, name const & e) {
|
||||
throw exception(sstream() << "invalid " << k << ", type of '" << e
|
||||
<< "' does not match any of the allowed expected types for " << k << "s\n"
|
||||
<< " Pi (x_1 : A_1) ... (x_n : A_n) (y: C x_1 ... x_n), D t_1 ... t_m\n"
|
||||
<< " Pi (x_1 : A_1) ... (x_n : A_n) (y: C x_1 ... x_n), Type\n"
|
||||
<< " Pi (x_1 : A_1) ... (x_n : A_n) (y: C x_1 ... x_n), A -> B");
|
||||
}
|
||||
|
||||
pair<name, name> tc_multigraph::validate(environment const & env, name const & e, unsigned num_args) {
|
||||
declaration const & d = env.get(e);
|
||||
expr type = d.get_type();
|
||||
for (unsigned i = 0; i < num_args; i++) {
|
||||
if (!is_pi(type)) {
|
||||
throw_ex(m_kind, e);
|
||||
}
|
||||
type = binding_body(type);
|
||||
}
|
||||
if (!is_pi(type)) {
|
||||
throw_ex(m_kind, e);
|
||||
}
|
||||
buffer<expr> args;
|
||||
expr const & C = get_app_args(binding_domain(type), args);
|
||||
if (!is_constant(C) || !check_levels(const_levels(C), d.get_univ_params()) || !check_var_args(args)) {
|
||||
throw_ex(m_kind, e);
|
||||
}
|
||||
name src = const_name(C);
|
||||
type = binding_body(type);
|
||||
name tgt;
|
||||
if (is_sort(type)) {
|
||||
tgt = *g_sort_sink;
|
||||
} else if (is_pi(type)) {
|
||||
tgt = *g_fun_sink;
|
||||
} else {
|
||||
expr const & D = get_app_fn(type);
|
||||
if (is_constant(D)) {
|
||||
tgt = const_name(D);
|
||||
} else {
|
||||
throw_ex(m_kind, e);
|
||||
}
|
||||
}
|
||||
if (src == tgt) {
|
||||
throw_ex(m_kind, e);
|
||||
}
|
||||
return mk_pair(src, tgt);
|
||||
}
|
||||
|
||||
pair<environment, list<name>> tc_multigraph::add(environment const & env, name const & e, unsigned num_args) {
|
||||
auto src_tgt = validate(env, e, num_args);
|
||||
return add_edge_fn(env, *this)(src_tgt.first, e, src_tgt.second);
|
||||
}
|
||||
|
||||
pair<environment, list<name>> tc_multigraph::add(environment const & env, name const & e) {
|
||||
declaration const & d = env.get(e);
|
||||
unsigned n = get_arity(d.get_type());
|
||||
if (n == 0)
|
||||
throw_ex(m_kind, e);
|
||||
return add(env, e, n-1);
|
||||
}
|
||||
|
||||
void tc_multigraph::add1(environment const & env, name const & e, unsigned num_args) {
|
||||
auto src_tgt = validate(env, e, num_args);
|
||||
return add_edge_fn(env, *this).add_core(src_tgt.first, e, src_tgt.second);
|
||||
}
|
||||
|
||||
void tc_multigraph::add1(environment const & env, name const & e) {
|
||||
declaration const & d = env.get(e);
|
||||
unsigned n = get_arity(d.get_type());
|
||||
if (n == 0)
|
||||
throw_ex(m_kind, e);
|
||||
return add1(env, e, n-1);
|
||||
}
|
||||
|
||||
bool tc_multigraph::is_fun_sink(name const & c) {
|
||||
return c == *g_fun_sink;
|
||||
}
|
||||
|
||||
bool tc_multigraph::is_sort_sink(name const & c) {
|
||||
return c == *g_sort_sink;
|
||||
}
|
||||
|
||||
void initialize_tc_multigraph() {
|
||||
name p = name::mk_internal_unique_name();
|
||||
g_fun_sink = new name(p, "Fun");
|
||||
g_sort_sink = new name(p, "Sort");
|
||||
}
|
||||
|
||||
void finalize_tc_multigraph() {
|
||||
delete g_fun_sink;
|
||||
delete g_sort_sink;
|
||||
}
|
||||
}
|
||||
|
|
|
@ -24,14 +24,5 @@ public:
|
|||
bool is_node(name const & c) const;
|
||||
list<pair<name, name>> get_successors(name const & c) const;
|
||||
list<name> get_predecessors(name const & c) const;
|
||||
// TODO(Leo): Remove the following methods. They should be part of the coercion management module.
|
||||
pair<environment, list<name>> add(environment const & env, name const & e, unsigned num_args);
|
||||
pair<environment, list<name>> add(environment const & env, name const & e);
|
||||
void add1(environment const & env, name const & e, unsigned num_args);
|
||||
void add1(environment const & env, name const & e);
|
||||
static bool is_fun_sink(name const & c);
|
||||
static bool is_sort_sink(name const & c);
|
||||
};
|
||||
void initialize_tc_multigraph();
|
||||
void finalize_tc_multigraph();
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue