From f75de2e950e3619b0e50464336337be1fb135f1f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 9 Aug 2016 16:27:33 -0700 Subject: [PATCH] chore(library/definitional,frontends/lean): remove decreasing macro --- src/frontends/lean/builtin_exprs.cpp | 1 - src/frontends/lean/old_elaborator.cpp | 36 ---------------------- src/frontends/lean/old_elaborator.h | 2 -- src/frontends/lean/token_table.cpp | 6 +--- src/frontends/lean/token_table.h | 1 - src/library/definitional/equations.cpp | 42 -------------------------- src/library/definitional/equations.h | 5 --- 7 files changed, 1 insertion(+), 92 deletions(-) diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index 9117f7ad51..4e0d168fb4 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -715,7 +715,6 @@ parse_table init_nud_table() { parse_table init_led_table() { parse_table r(false); r = r.add({transition("->", mk_expr_action(get_arrow_prec()-1))}, mk_arrow(Var(1), Var(1))); - r = r.add({transition(" ts; - old_type_checker & tc = *m_tc; - to_telescope(tc, f_type, ts, optional(), cs); - buffer old_args; - buffer new_args; - get_app_args(*m_equation_lhs, old_args); - get_app_args(dec_app, new_args); - if (new_args.size() != old_args.size() || new_args.size() != ts.size()) - throw_elaborator_exception("invalid recursive application, mistmatch in the number of arguments", e); - expr old_tuple = mk_sigma_mk(tc, ts, old_args, cs); - expr new_tuple = mk_sigma_mk(tc, ts, new_args, cs); - expr expected_dec_proof_type = mk_app(mk_app(*m_equation_R, new_tuple, e.get_tag()), old_tuple, e.get_tag()); - expr dec_proof_type = infer_type(dec_proof, cs); - justification j = mk_type_mismatch_jst(dec_proof, dec_proof_type, expected_dec_proof_type, decreasing_proof(e)); - auto new_dec_proof_cs = ensure_has_type(dec_proof, dec_proof_type, expected_dec_proof_type, j); - dec_proof = new_dec_proof_cs.first; - cs += new_dec_proof_cs.second; - return mk_decreasing(dec_app, dec_proof); -} - bool old_elaborator::is_structure_like(expr const & S) { expr const & I = get_app_fn(S); return is_constant(I) && ::lean::is_structure_like(env(), const_name(I)); @@ -1385,8 +1351,6 @@ expr old_elaborator::visit_core(expr const & e, constraint_seq & cs) { return visit_equation(e, cs); } else if (is_inaccessible(e)) { return visit_inaccessible(e, cs); - } else if (is_decreasing(e)) { - return visit_decreasing(e, cs); } else if (is_structure_instance(e)) { return visit_structure_instance(e, cs); } else if (is_checkpoint_annotation(e)) { diff --git a/src/frontends/lean/old_elaborator.h b/src/frontends/lean/old_elaborator.h index 1ef0ca186d..a0640ef4eb 100644 --- a/src/frontends/lean/old_elaborator.h +++ b/src/frontends/lean/old_elaborator.h @@ -49,7 +49,6 @@ class old_elaborator { // and inaccessible expressions are allowed bool m_in_equation_lhs; // if m_equation_lhs is not none, we are processing the right-hand-side of an equation - // and decreasing expressions are allowed optional m_equation_lhs; // if m_equation_R is not none when elaborator is processing recursive equation using the well-founded relation R. optional m_equation_R; @@ -162,7 +161,6 @@ class old_elaborator { expr visit_equations(expr const & eqns, constraint_seq & cs); expr visit_equation(expr const & e, constraint_seq & cs); expr visit_inaccessible(expr const & e, constraint_seq & cs); - expr visit_decreasing(expr const & e, constraint_seq & cs); constraint mk_equations_cnstr(expr const & m, expr const & eqns); bool is_structure_like(expr const & S); diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index e4784a924e..0c85ab593b 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -12,7 +12,6 @@ Author: Leonardo de Moura namespace lean { static unsigned g_arrow_prec = 25; -static unsigned g_decreasing_prec = 100; static unsigned g_max_prec = 1024; static unsigned g_Max_prec = 1024*1024; static unsigned g_plus_prec = 65; @@ -20,7 +19,6 @@ static unsigned g_cup_prec = 60; unsigned get_max_prec() { return g_max_prec; } unsigned get_Max_prec() { return g_Max_prec; } unsigned get_arrow_prec() { return g_arrow_prec; } -unsigned get_decreasing_prec() { return g_decreasing_prec; } static token_table update(token_table const & s, char const * token, char const * val, optional expr_prec, optional tac_prec) { lean_assert(expr_prec || tac_prec); @@ -85,7 +83,6 @@ static char const * g_forall_unicode = "\u2200"; static char const * g_arrow_unicode = "\u2192"; static char const * g_cup = "\u2294"; static char const * g_qed_unicode = "∎"; -static char const * g_decreasing_unicode = "↓"; void init_token_table(token_table & t) { pair builtin[] = @@ -102,7 +99,7 @@ void init_token_table(token_table & t) { {"@@", g_max_prec}, {"@", g_max_prec}, {"sorry", g_max_prec}, {"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec}, {"<-", 0}, {"?(", g_max_prec}, {"⌞", g_max_prec}, {"⌟", 0}, {"match", 0}, - {"", get_arrow_prec()); t = add_token(t, "←", "<-", 0); - t = add_token(t, g_decreasing_unicode, "first) { diff --git a/src/frontends/lean/token_table.h b/src/frontends/lean/token_table.h index 49ef9dc760..0508c7d2ac 100644 --- a/src/frontends/lean/token_table.h +++ b/src/frontends/lean/token_table.h @@ -20,7 +20,6 @@ unsigned get_max_prec(); // Internal maximum precedence used for @@, @ and ! operators unsigned get_Max_prec(); unsigned get_arrow_prec(); -unsigned get_decreasing_prec(); class token_info { bool m_command; name m_token; diff --git a/src/library/definitional/equations.cpp b/src/library/definitional/equations.cpp index 1cf949c677..1732052d7a 100644 --- a/src/library/definitional/equations.cpp +++ b/src/library/definitional/equations.cpp @@ -33,13 +33,11 @@ namespace lean { static name * g_equations_name = nullptr; static name * g_equation_name = nullptr; static name * g_no_equation_name = nullptr; -static name * g_decreasing_name = nullptr; static name * g_inaccessible_name = nullptr; static name * g_equations_result_name = nullptr; static std::string * g_equations_opcode = nullptr; static std::string * g_equation_opcode = nullptr; static std::string * g_no_equation_opcode = nullptr; -static std::string * g_decreasing_opcode = nullptr; static std::string * g_equations_result_opcode = nullptr; [[ noreturn ]] static void throw_eqs_ex() { throw exception("unexpected occurrence of 'equations' expression"); } @@ -80,28 +78,8 @@ public: virtual void write(serializer & s) const { s.write_string(*g_no_equation_opcode); } }; -class decreasing_macro_cell : public macro_definition_cell { - void check_macro(expr const & m) const { - if (!is_macro(m) || macro_num_args(m) != 2) - throw exception("invalid 'decreasing' expression, incorrect number of arguments"); - } -public: - decreasing_macro_cell() {} - virtual name get_name() const { return *g_decreasing_name; } - virtual expr check_type(expr const & m, abstract_type_context & ctx, bool infer_only) const { - check_macro(m); - return ctx.check(macro_arg(m, 0), infer_only); - } - virtual optional expand(expr const & m, abstract_type_context &) const { - check_macro(m); - return some_expr(macro_arg(m, 0)); - } - virtual void write(serializer & s) const { s.write_string(*g_decreasing_opcode); } -}; - static macro_definition * g_equation = nullptr; static macro_definition * g_no_equation = nullptr; -static macro_definition * g_decreasing = nullptr; bool is_equation(expr const & e) { return is_macro(e) && macro_def(e) == *g_equation; } @@ -128,14 +106,6 @@ bool is_lambda_no_equation(expr const & e) { return is_no_equation(e); } -bool is_decreasing(expr const & e) { return is_macro(e) && macro_def(e) == *g_decreasing; } -expr const & decreasing_app(expr const & e) { lean_assert(is_decreasing(e)); return macro_arg(e, 0); } -expr const & decreasing_proof(expr const & e) { lean_assert(is_decreasing(e)); return macro_arg(e, 1); } -expr mk_decreasing(expr const & t, expr const & H) { - expr args[2] = { t, H }; - return mk_macro(*g_decreasing, 2, args); -} - bool is_equations(expr const & e) { return is_macro(e) && macro_def(e).get_name() == *g_equations_name; } bool is_wf_equations_core(expr const & e) { lean_assert(is_equations(e)); @@ -230,17 +200,14 @@ void initialize_equations() { g_equations_name = new name("equations"); g_equation_name = new name("equation"); g_no_equation_name = new name("no_equation"); - g_decreasing_name = new name("decreasing"); g_inaccessible_name = new name("innaccessible"); g_equations_result_name = new name("equations_result"); g_equation = new macro_definition(new equation_macro_cell()); g_no_equation = new macro_definition(new no_equation_macro_cell()); - g_decreasing = new macro_definition(new decreasing_macro_cell()); g_equations_result = new macro_definition(new equations_result_macro_cell()); g_equations_opcode = new std::string("Eqns"); g_equation_opcode = new std::string("Eqn"); g_no_equation_opcode = new std::string("NEqn"); - g_decreasing_opcode = new std::string("Decr"); g_equations_result_opcode = new std::string("EqnR"); register_annotation(*g_inaccessible_name); register_macro_deserializer(*g_equations_opcode, @@ -269,12 +236,6 @@ void initialize_equations() { throw corrupted_stream_exception(); return mk_no_equation(); }); - register_macro_deserializer(*g_decreasing_opcode, - [](deserializer &, unsigned num, expr const * args) { - if (num != 2) - throw corrupted_stream_exception(); - return mk_decreasing(args[0], args[1]); - }); register_macro_deserializer(*g_equations_result_opcode, [](deserializer &, unsigned num, expr const * args) { return mk_equations_result(num, args); @@ -286,16 +247,13 @@ void finalize_equations() { delete g_equation_opcode; delete g_no_equation_opcode; delete g_equations_opcode; - delete g_decreasing_opcode; delete g_equations_result; delete g_equation; delete g_no_equation; - delete g_decreasing; delete g_equations_result_name; delete g_equations_name; delete g_equation_name; delete g_no_equation_name; - delete g_decreasing_name; delete g_inaccessible_name; } diff --git a/src/library/definitional/equations.h b/src/library/definitional/equations.h index 547e04f738..3bfd19b1bc 100644 --- a/src/library/definitional/equations.h +++ b/src/library/definitional/equations.h @@ -22,11 +22,6 @@ bool is_lambda_equation(expr const & e); expr mk_no_equation(); bool is_no_equation(expr const & e); -bool is_decreasing(expr const & e); -expr const & decreasing_app(expr const & e); -expr const & decreasing_proof(expr const & e); -expr mk_decreasing(expr const & t, expr const & H); - bool is_equations(expr const & e); bool is_wf_equations(expr const & e); unsigned equations_size(expr const & e);