From 3ca785b0e77432c4efd5f15d9c69075cdd863c5d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 6 Jan 2016 17:29:02 -0800 Subject: [PATCH] refactor(library/fun_info_manager): remove dead code --- src/frontends/lean/builtin_cmds.cpp | 36 ---------- src/frontends/lean/token_table.cpp | 2 +- src/library/fun_info_manager.cpp | 99 --------------------------- src/library/fun_info_manager.h | 24 ------- tests/lean/replace1.lean | 41 ----------- tests/lean/replace1.lean.expected.out | 20 ------ 6 files changed, 1 insertion(+), 221 deletions(-) delete mode 100644 tests/lean/replace1.lean delete mode 100644 tests/lean/replace1.lean.expected.out diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 8ff70436a..0995eac70 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -655,41 +655,6 @@ static environment trans_cmd(parser & p) { return env; } -static void parse_expr_vector(parser & p, buffer & 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 from; - buffer 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)); diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index fd83cc554..ae01d9b98 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -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 aliases[] = {{g_lambda_unicode, "fun"}, {"forall", "Pi"}, {g_forall_unicode, "Pi"}, {g_pi_unicode, "Pi"}, diff --git a/src/library/fun_info_manager.cpp b/src/library/fun_info_manager.cpp index f9776e951..94b92f0f4 100644 --- a/src/library/fun_info_manager.cpp +++ b/src/library/fun_info_manager.cpp @@ -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 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 new_args; - buffer 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 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(); - } -} } diff --git a/src/library/fun_info_manager.h b/src/library/fun_info_manager.h index 5f419a15a..5305e9a91 100644 --- a/src/library/fun_info_manager.h +++ b/src/library/fun_info_manager.h @@ -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 replace(fun_info_manager & infom, expr const & e, unsigned n, expr const * ts, expr const * rs); -inline optional replace(fun_info_manager & infom, expr const & e, buffer const & ts, buffer const & rs) { - lean_assert(ts.size() == rs.size()); - return replace(infom, e, ts.size(), ts.data(), rs.data()); -} } diff --git a/tests/lean/replace1.lean b/tests/lean/replace1.lean deleted file mode 100644 index 7629fecd7..000000000 --- a/tests/lean/replace1.lean +++ /dev/null @@ -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)] diff --git a/tests/lean/replace1.lean.expected.out b/tests/lean/replace1.lean.expected.out deleted file mode 100644 index c1828b8e8..000000000 --- a/tests/lean/replace1.lean.expected.out +++ /dev/null @@ -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₂