refactor(library/fun_info_manager): remove dead code
This commit is contained in:
Leonardo de Moura
parent
a992bb46a6
commit
3ca785b0e7
6 changed files with 1 additions and 221 deletions
|
|
@ -655,41 +655,6 @@ static environment trans_cmd(parser & p) {
|
|||
return env;
|
||||
}
|
||||
|
||||
static void parse_expr_vector(parser & p, buffer<expr> & r) {
|
||||
p.check_token_next(get_lbracket_tk(), "invalid command, '[' expected");
|
||||
while (true) {
|
||||
expr e; level_param_names ls;
|
||||
std::tie(e, ls) = parse_local_expr(p);
|
||||
r.push_back(e);
|
||||
if (!p.curr_is_token(get_comma_tk()))
|
||||
break;
|
||||
p.next();
|
||||
}
|
||||
p.check_token_next(get_rbracket_tk(), "invalid command, ']' expected");
|
||||
}
|
||||
|
||||
static environment replace_cmd(parser & p) {
|
||||
environment const & env = p.env();
|
||||
auto pos = p.pos();
|
||||
expr e; level_param_names ls;
|
||||
buffer<expr> from;
|
||||
buffer<expr> to;
|
||||
std::tie(e, ls) = parse_local_expr(p);
|
||||
p.check_token_next(get_comma_tk(), "invalid #replace command, ',' expected");
|
||||
parse_expr_vector(p, from);
|
||||
p.check_token_next(get_comma_tk(), "invalid #replace command, ',' expected");
|
||||
parse_expr_vector(p, to);
|
||||
if (from.size() != to.size())
|
||||
throw parser_error("invalid #replace command, from/to vectors have different size", pos);
|
||||
tmp_type_context ctx(env, p.get_options());
|
||||
fun_info_manager infom(ctx);
|
||||
auto r = replace(infom, e, from, to);
|
||||
if (!r)
|
||||
throw parser_error("#replace commad failed", pos);
|
||||
p.regular_stream() << *r << "\n";
|
||||
return env;
|
||||
}
|
||||
|
||||
enum class congr_kind { Simp, Default, Rel };
|
||||
|
||||
static environment congr_cmd_core(parser & p, congr_kind kind) {
|
||||
|
|
@ -849,7 +814,6 @@ void init_cmd_table(cmd_table & r) {
|
|||
add_cmd(r, cmd_info("#trans", "(for debugging purposes)", trans_cmd));
|
||||
add_cmd(r, cmd_info("#symm", "(for debugging purposes)", symm_cmd));
|
||||
add_cmd(r, cmd_info("#compile", "(for debugging purposes)", compile_cmd));
|
||||
add_cmd(r, cmd_info("#replace", "(for debugging purposes)", replace_cmd));
|
||||
add_cmd(r, cmd_info("#congr", "(for debugging purposes)", congr_cmd));
|
||||
add_cmd(r, cmd_info("#congr_simp", "(for debugging purposes)", congr_simp_cmd));
|
||||
add_cmd(r, cmd_info("#congr_rel", "(for debugging purposes)", congr_rel_cmd));
|
||||
|
|
|
|||
|
|
@ -120,7 +120,7 @@ void init_token_table(token_table & t) {
|
|||
"multiple_instances", "find_decl", "attribute", "persistent",
|
||||
"include", "omit", "migrate", "init_quotient", "init_hits", "#erase_cache", "#projections", "#telescope_eq",
|
||||
"#compile", "#accessible", "#decl_stats", "#relevant_thms", "#simplify", "#app_builder", "#refl", "#symm",
|
||||
"#trans", "#replace", "#congr", "#congr_simp", "#congr_rel", "#normalizer", "#abstract_expr", nullptr};
|
||||
"#trans", "#congr", "#congr_simp", "#congr_rel", "#normalizer", "#abstract_expr", nullptr};
|
||||
|
||||
pair<char const *, char const *> aliases[] =
|
||||
{{g_lambda_unicode, "fun"}, {"forall", "Pi"}, {g_forall_unicode, "Pi"}, {g_pi_unicode, "Pi"},
|
||||
|
|
|
|||
|
|
@ -88,103 +88,4 @@ fun_info fun_info_manager::get_specialization(expr const &) {
|
|||
// TODO(Leo)
|
||||
lean_unreachable();
|
||||
}
|
||||
|
||||
struct replace_fn : public replace_visitor {
|
||||
fun_info_manager & m_infom;
|
||||
type_context & m_ctx;
|
||||
unsigned m_num;
|
||||
expr const * m_from;
|
||||
expr const * m_to;
|
||||
|
||||
struct failed {};
|
||||
|
||||
replace_fn(fun_info_manager & infom, unsigned n, expr const * ts, expr const * rs):
|
||||
m_infom(infom), m_ctx(infom.ctx()), m_num(n), m_from(ts), m_to(rs) {}
|
||||
|
||||
virtual expr visit(expr const & e) {
|
||||
for (unsigned i = 0; i < m_num; i++) {
|
||||
if (e == m_from[i])
|
||||
return m_to[i];
|
||||
}
|
||||
return replace_visitor::visit(e);
|
||||
}
|
||||
|
||||
virtual expr visit_mlocal(expr const & e) {
|
||||
return e;
|
||||
}
|
||||
|
||||
virtual expr visit_binding(expr const & b) {
|
||||
expr new_domain = visit(binding_domain(b));
|
||||
expr l = m_ctx.mk_tmp_local(binding_name(b), new_domain, binding_info(b));
|
||||
expr new_body = abstract(visit(instantiate(binding_body(b), l)), l);
|
||||
return update_binding(b, new_domain, new_body);
|
||||
}
|
||||
|
||||
virtual expr visit_app(expr const & e) {
|
||||
buffer<expr> args;
|
||||
expr f = get_app_args(e, args);
|
||||
expr new_f = visit(f);
|
||||
fun_info info = m_infom.get(f);
|
||||
if (info.get_arity() < args.size())
|
||||
throw failed();
|
||||
auto ps_info = info.get_params_info();
|
||||
bool modified = f != new_f;
|
||||
buffer<expr> new_args;
|
||||
buffer<bool> to_check;
|
||||
bool has_to_check = false;
|
||||
for (expr const & arg : args) {
|
||||
expr new_arg = visit(arg);
|
||||
auto pinfo = head(ps_info);
|
||||
bool c = false;
|
||||
if (modified) {
|
||||
// if not argument has been modified, then there is nothing to be checked
|
||||
for (unsigned idx : pinfo.get_dependencies()) {
|
||||
lean_assert(idx < new_args.size());
|
||||
if (args[idx] != new_args[idx]) {
|
||||
c = true;
|
||||
has_to_check = true;
|
||||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
if (new_arg != arg) {
|
||||
modified = true;
|
||||
}
|
||||
to_check.push_back(c);
|
||||
new_args.push_back(new_arg);
|
||||
ps_info = tail(ps_info);
|
||||
}
|
||||
lean_assert(args.size() == new_args.size());
|
||||
if (!modified)
|
||||
return e;
|
||||
expr new_e = mk_app(new_f, new_args);
|
||||
if (has_to_check) {
|
||||
lean_assert(to_check.size() == new_args.size());
|
||||
expr it = new_e;
|
||||
unsigned i = to_check.size();
|
||||
while (i > 0) {
|
||||
--i;
|
||||
expr const & fn = app_fn(it);
|
||||
if (to_check[i]) {
|
||||
expr fn_type = m_ctx.whnf(m_ctx.infer(fn));
|
||||
if (!is_pi(fn_type))
|
||||
throw failed();
|
||||
expr arg_type = m_ctx.infer(app_arg(it));
|
||||
if (!m_ctx.is_def_eq(binding_domain(fn_type), arg_type))
|
||||
throw failed();
|
||||
}
|
||||
it = fn;
|
||||
}
|
||||
}
|
||||
return new_e;
|
||||
}
|
||||
};
|
||||
|
||||
optional<expr> replace(fun_info_manager & infom, expr const & e, unsigned n, expr const * ts, expr const * rs) {
|
||||
try {
|
||||
return some_expr(replace_fn(infom, n, ts, rs)(e));
|
||||
} catch (replace_fn::failed &) {
|
||||
return none_expr();
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -99,28 +99,4 @@ public:
|
|||
is_prop and is_subsingleton. */
|
||||
fun_info get_specialization(expr const & app);
|
||||
};
|
||||
|
||||
/** \brief Given a term \c e of the form F[ts[0], ..., ts[n-1]],
|
||||
return F[rs[0], ..., rs[n-1]] only if the replacement does not produce type errors.
|
||||
|
||||
Note that even if each ts[i] and rs[i] have the same type, the result may be none.
|
||||
|
||||
Here is a very simple example:
|
||||
Given (f : Pi (n : nat), bv n -> bv n) (v : bv 10), then (F[v] := f 10 v) is type
|
||||
correct, but (f 11 v) is not.
|
||||
|
||||
If
|
||||
a) F[ts[0], ..., ts[n-1] is type correct, and
|
||||
b) If there is a telescope T s.t. (ts[0], ..., ts[n-1]) and (rs[0], ..., rs[n-1]) are instances of T, and
|
||||
c) the result is not none
|
||||
Then
|
||||
the result is type correct.
|
||||
|
||||
TODO(Leo): move to a different file?
|
||||
*/
|
||||
optional<expr> replace(fun_info_manager & infom, expr const & e, unsigned n, expr const * ts, expr const * rs);
|
||||
inline optional<expr> replace(fun_info_manager & infom, expr const & e, buffer<expr> const & ts, buffer<expr> const & rs) {
|
||||
lean_assert(ts.size() == rs.size());
|
||||
return replace(infom, e, ts.size(), ts.data(), rs.data());
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,41 +0,0 @@
|
|||
constant f : Π {A : Type}, A → A → A
|
||||
variables a b c : nat
|
||||
variables H : a = b
|
||||
|
||||
set_option pp.all true
|
||||
|
||||
#replace f a a, [a], [b]
|
||||
#replace f (f a b) b, [a,b], [b,a]
|
||||
|
||||
variables x y : bool
|
||||
|
||||
-- [nat] and [bool] are instances of the telescope (A : Type),
|
||||
-- but the resulting expression is type incorrect.
|
||||
-- Thus, #replace correctly detects the error.
|
||||
#replace f a a, [nat], [bool] -- Error
|
||||
-- An error is not detected in the following one,
|
||||
-- since there is no telescope s.t., [a] and [x] are instances of.
|
||||
#replace f a a, [a], [x]
|
||||
-- The following should work, [nat, a] and [bool, x] are instances
|
||||
-- of the telescope (A : Type, a : A), and the result is type correct
|
||||
#replace f a a, [nat, a], [bool, x]
|
||||
|
||||
variable p : nat → Prop
|
||||
variable H1 : p a
|
||||
|
||||
-- [b] and [a] are instances of the telescope (x : nat),
|
||||
-- but the resulting expression is type incorrect.
|
||||
-- Thus, #replace correctly detects the error.
|
||||
#replace @eq.rec nat a (λ x : nat, p x) H1 b H, [b], [a] -- Error
|
||||
-- There is no telescope s.t. [H] and [eq.refl a] are instances of.
|
||||
#replace @eq.rec nat a (λ x : nat, p x) H1 b H, [H], [eq.refl a]
|
||||
-- [b, H] and [a, eq.refl a] are both instances of the telescope
|
||||
-- (x : nat, H : a = x), and the resulting expression is type correct
|
||||
#replace @eq.rec nat a (λ x : nat, p x) H1 b H, [b, H], [a, eq.refl a]
|
||||
|
||||
constant bv : nat → Type₁
|
||||
|
||||
variables v₁ v₂ : bv 10
|
||||
|
||||
#replace v₁ = v₂, [(10:nat)], [(11:nat)] -- Error
|
||||
#replace (λ v₁ v₂ : bv 10, v₁ = v₂), [(10:nat)], [(11:nat)]
|
||||
|
|
@ -1,20 +0,0 @@
|
|||
@f.{1} nat b b
|
||||
@f.{1} nat (@f.{1} nat b a) a
|
||||
replace1.lean:15:9: error: #replace commad failed
|
||||
@f.{1} nat x x
|
||||
@f.{1} bool x x
|
||||
replace1.lean:29:9: error: #replace commad failed
|
||||
@eq.rec.{0 1} nat a (λ (x : nat), p x) H1 b (@eq.refl.{1} nat a)
|
||||
@eq.rec.{0 1} nat a (λ (x : nat), p x) H1 a (@eq.refl.{1} nat a)
|
||||
replace1.lean:40:9: error: #replace commad failed
|
||||
λ
|
||||
(v₁ v₂ :
|
||||
bv
|
||||
(@bit1.{1} nat nat_has_one nat_has_add
|
||||
(@bit1.{1} nat nat_has_one nat_has_add (@bit0.{1} nat nat_has_add (@one.{1} nat nat_has_one))))),
|
||||
@eq.{1}
|
||||
(bv
|
||||
(@bit1.{1} nat nat_has_one nat_has_add
|
||||
(@bit1.{1} nat nat_has_one nat_has_add (@bit0.{1} nat nat_has_add (@one.{1} nat nat_has_one)))))
|
||||
v₁
|
||||
v₂
|
||||
Loading…
Reference in a new issue