From b53e6eda58882c089383143dbac2ea7ec83c122a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 14 Jul 2014 05:41:44 +0100 Subject: [PATCH] refactor(frontends/lean): eliminate the abstract method 'family' from parser Signed-off-by: Leonardo de Moura --- src/frontends/lean/builtin_exprs.cpp | 7 ++++--- src/frontends/lean/decl_cmds.cpp | 17 +++++++++-------- src/frontends/lean/inductive_cmd.cpp | 9 +++++---- src/frontends/lean/parser.cpp | 11 +++++------ src/frontends/lean/parser.h | 6 ------ src/frontends/lean/parser_bindings.cpp | 5 +++-- src/frontends/lean/util.cpp | 8 ++++++++ src/frontends/lean/util.h | 4 ++++ 8 files changed, 38 insertions(+), 29 deletions(-) diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index f07c0cbc8..e6c754e11 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -15,6 +15,7 @@ Author: Leonardo de Moura #include "frontends/lean/calc.h" #include "frontends/lean/proof_qed_ext.h" #include "frontends/lean/parser.h" +#include "frontends/lean/util.h" namespace lean { namespace notation { @@ -109,8 +110,8 @@ static expr parse_let(parser & p, pos_info const & pos) { p.check_token_next(g_assign, "invalid let declaration, ':=' expected"); value = p.parse_scoped_expr(ps, lenv); if (is_opaque) - type = p.pi_abstract(ps, type); - value = p.lambda_abstract(ps, value); + type = Pi(ps, type, p); + value = Fun(ps, value, p); } if (is_opaque) { expr l = p.save_pos(mk_local(id, type), pos); @@ -356,7 +357,7 @@ static expr parse_including_expr(parser & p, unsigned, expr const *, pos_info co p.add_local(new_l); new_locals.push_back(new_l); } - expr r = p.rec_save_pos(Fun(new_locals, p.parse_expr()), pos); + expr r = Fun(new_locals, p.parse_expr(), p); r = p.rec_save_pos(mk_app(r, locals), pos); return r; } diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index 028dd1d8f..65bd9fde3 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/src/frontends/lean/decl_cmds.cpp @@ -7,6 +7,7 @@ Author: Leonardo de Moura #include #include "util/sstream.h" #include "kernel/type_checker.h" +#include "kernel/abstract.h" #include "library/scoped_ext.h" #include "library/aliases.h" #include "library/private.h" @@ -124,7 +125,7 @@ environment variable_cmd_core(parser & p, bool is_axiom) { auto lenv = p.parse_binders(ps); p.check_token_next(g_colon, "invalid declaration, ':' expected"); type = p.parse_scoped_expr(ps, lenv); - type = p.pi_abstract(ps, type); + type = Pi(ps, type, p); } else { p.next(); type = p.parse_expr(); @@ -230,9 +231,9 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) { buffer ps; optional lenv; lenv = p.parse_binders(ps); + auto pos = p.pos(); if (p.curr_is_token(g_colon)) { p.next(); - auto pos = p.pos(); type = p.parse_scoped_expr(ps, *lenv); if (is_theorem && !p.curr_is_token(g_assign)) { value = p.save_pos(mk_expr_placeholder(), pos); @@ -245,8 +246,8 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) { p.check_token_next(g_assign, "invalid declaration, ':=' expected"); value = p.parse_scoped_expr(ps, *lenv); } - type = p.pi_abstract(ps, type); - value = p.lambda_abstract(ps, value); + type = Pi(ps, type, p); + value = Fun(ps, value, p); } update_univ_parameters(ls_buffer, collect_univ_params(value, collect_univ_params(type)), p); ls = to_list(ls_buffer.begin(), ls_buffer.end()); @@ -254,14 +255,12 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) { if (in_section(env)) { buffer section_ps; collect_section_locals(type, value, p, section_ps); - type = p.pi_abstract(section_ps, type); - value = p.lambda_abstract(section_ps, value); + type = Pi(section_ps, type, p); + value = Fun(section_ps, value, p); levels section_ls = collect_section_levels(ls, p); expr ref = mk_app(mk_explicit(mk_constant(real_n, section_ls)), section_ps); p.add_local_expr(n, ref); } - if (real_n != n) - env = add_decl_alias(env, n, mk_constant(real_n)); level_param_names new_ls; if (is_theorem) { if (p.num_threads() > 1) { @@ -285,6 +284,8 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) { std::tie(type, value, new_ls) = p.elaborate_definition(n, type, value); env = module::add(env, check(env, mk_definition(env, real_n, append(ls, new_ls), type, value, modifiers.m_is_opaque))); } + if (real_n != n) + env = add_decl_alias(env, n, mk_constant(real_n)); if (modifiers.m_is_instance) env = add_instance(env, real_n); if (modifiers.m_is_coercion) diff --git a/src/frontends/lean/inductive_cmd.cpp b/src/frontends/lean/inductive_cmd.cpp index 19bfbb148..52c6b6427 100644 --- a/src/frontends/lean/inductive_cmd.cpp +++ b/src/frontends/lean/inductive_cmd.cpp @@ -11,6 +11,7 @@ Author: Leonardo de Moura #include "kernel/type_checker.h" #include "kernel/instantiate.h" #include "kernel/inductive/inductive.h" +#include "kernel/abstract.h" #include "kernel/free_vars.h" #include "library/scoped_ext.h" #include "library/locals.h" @@ -150,7 +151,7 @@ struct inductive_cmd_fn { m_p.parse_binders(ps); m_p.check_token_next(g_colon, "invalid inductive declaration, ':' expected"); type = m_p.parse_scoped_expr(ps); - type = m_p.pi_abstract(ps, type); + type = Pi(ps, type, m_p); } else { m_p.next(); type = m_p.parse_expr(); @@ -263,7 +264,7 @@ struct inductive_cmd_fn { } m_p.check_token_next(g_colon, "invalid introduction rule, ':' expected"); expr intro_type = m_p.parse_scoped_expr(params, m_env); - intro_type = m_p.pi_abstract(params, intro_type); + intro_type = Pi(params, intro_type, m_p); intro_type = infer_implicit(intro_type, params.size(), strict); intros.push_back(intro_rule(intro_name, intro_type)); } @@ -365,7 +366,7 @@ struct inductive_cmd_fn { sort_section_params(section_locals, m_p, section_params); // First, add section_params to inductive types type. for (inductive_decl & d : decls) { - d = update_inductive_decl(d, m_p.pi_abstract(section_params, inductive_decl_type(d))); + d = update_inductive_decl(d, Pi(section_params, inductive_decl_type(d), m_p)); } // Add section_params to introduction rules type, and also "fix" // occurrences of inductive types. @@ -374,7 +375,7 @@ struct inductive_cmd_fn { for (auto const & ir : inductive_decl_intros(d)) { expr type = intro_rule_type(ir); type = fix_inductive_occs(type, decls, section_params); - type = m_p.pi_abstract(section_params, type); + type = Pi(section_params, type, m_p); bool strict = m_relaxed_implicit_infer.contains(intro_rule_name(ir)); type = infer_implicit(type, section_params.size(), strict); new_irs.push_back(update_intro_rule(ir, type)); diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 580d4bf07..a8d0a4dc8 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -729,7 +729,11 @@ expr parser::parse_notation(parse_table t, expr * left) { case notation::action_kind::ScopedExpr: { expr r = parse_scoped_expr(ps, lenv, a.rbp()); if (is_var(a.get_rec(), 0)) { - r = abstract(ps, r, a.use_lambda_abstraction(), binder_pos); + if (a.use_lambda_abstraction()) + r = Fun(ps, r); + else + r = Pi(ps, r); + r = rec_save_pos(r, binder_pos); } else { expr rec = copy_with_new_pos(a.get_rec(), p); unsigned i = ps.size(); @@ -942,11 +946,6 @@ expr parser::parse_scoped_expr(unsigned num_ps, expr const * ps, local_environme return parse_expr(rbp); } -expr parser::abstract(unsigned num_ps, expr const * ps, expr const & e, bool lambda, pos_info const & p) { - expr r = lambda ? Fun(num_ps, ps, e) : Pi(num_ps, ps, e); - return rec_save_pos(r, p); -} - void parser::parse_command() { lean_assert(curr() == scanner::token_kind::CommandKeyword); m_last_cmd_pos = pos(); diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index 1d41f9c79..bfe6fe278 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -231,12 +231,6 @@ public: return parse_scoped_expr(num_params, ps, local_environment(m_env), rbp); } expr parse_scoped_expr(buffer & ps, unsigned rbp = 0) { return parse_scoped_expr(ps.size(), ps.data(), rbp); } - expr abstract(unsigned num_params, expr const * ps, expr const & e, bool lambda, pos_info const & p); - expr abstract(buffer const & ps, expr const & e, bool lambda, pos_info const & p) { return abstract(ps.size(), ps.data(), e, lambda, p); } - expr lambda_abstract(buffer const & ps, expr const & e, pos_info const & p) { return abstract(ps, e, true, p); } - expr pi_abstract(buffer const & ps, expr const & e, pos_info const & p) { return abstract(ps, e, false, p); } - expr lambda_abstract(buffer const & ps, expr const & e) { return lambda_abstract(ps, e, pos_of(e)); } - expr pi_abstract(buffer const & ps, expr const & e) { return pi_abstract(ps, e, pos_of(e)); } struct local_scope { parser & m_p; environment m_env; local_scope(parser & p); ~local_scope(); }; void add_local_level(name const & n, level const & l); diff --git a/src/frontends/lean/parser_bindings.cpp b/src/frontends/lean/parser_bindings.cpp index ef236c9ad..44298f3ef 100644 --- a/src/frontends/lean/parser_bindings.cpp +++ b/src/frontends/lean/parser_bindings.cpp @@ -6,6 +6,7 @@ Author: Leonardo de Moura */ #include #include +#include "kernel/abstract.h" #include "frontends/lean/parser_bindings.h" namespace lean { @@ -96,9 +97,9 @@ static int lambda_abstract(lua_State * L) { expr const & e = to_expr(L, 2); expr r; if (nargs == 2) - r = gparser.abstract(s->second.size(), s->second.data(), e, true, gparser.pos_of(e)); + r = gparser.rec_save_pos(Fun(s->second.size(), s->second.data(), e), gparser.pos_of(e)); else - r = gparser.abstract(s->second.size(), s->second.data(), e, true, pos_info(lua_tointeger(L, 3), lua_tointeger(L, 4))); + r = gparser.rec_save_pos(Fun(s->second.size(), s->second.data(), e), pos_info(lua_tointeger(L, 3), lua_tointeger(L, 4))); return push_expr(L, r); } static int next(lua_State * L) { gparser.next(); return 0; } diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp index b72edace1..be92b351f 100644 --- a/src/frontends/lean/util.cpp +++ b/src/frontends/lean/util.cpp @@ -67,4 +67,12 @@ list locals_to_context(expr const & e, parser const & p) { std::reverse(locals.begin(), locals.end()); return to_list(locals.begin(), locals.end()); } + +expr Fun(buffer const & locals, expr const & e, parser & p) { + return p.rec_save_pos(Fun(locals, e), p.pos_of(e)); +} + +expr Pi(buffer const & locals, expr const & e, parser & p) { + return p.rec_save_pos(Pi(locals, e), p.pos_of(e)); +} } diff --git a/src/frontends/lean/util.h b/src/frontends/lean/util.h index 5717c9c58..a9859da4e 100644 --- a/src/frontends/lean/util.h +++ b/src/frontends/lean/util.h @@ -20,4 +20,8 @@ void collect_section_locals(expr const & type, expr const & value, parser const /** \brief Copy the local parameters to \c section_ps, then sort \c section_ps (using the order in which they were declared). */ void sort_section_params(expr_struct_set const & locals, parser const & p, buffer & section_ps); list locals_to_context(expr const & e, parser const & p); +/** \brief Fun(locals, e), but also propagate \c e position to result */ +expr Fun(buffer const & locals, expr const & e, parser & p); +/** \brief Pi(locals, e), but also propagate \c e position to result */ +expr Pi(buffer const & locals, expr const & e, parser & p); }