From 371dd9d1e1a17ce448ae24ca3fe0139a7146d2c8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 8 Aug 2016 09:05:22 -0700 Subject: [PATCH] refactor(frontends/lean): move match-expr parser to different module --- src/frontends/lean/CMakeLists.txt | 1 + src/frontends/lean/builtin_exprs.cpp | 1 + src/frontends/lean/decl_cmds.cpp | 55 -------------------- src/frontends/lean/decl_cmds.h | 19 +++---- src/frontends/lean/init_module.cpp | 3 ++ src/frontends/lean/match_expr.cpp | 72 +++++++++++++++++++++++++++ src/frontends/lean/match_expr.h | 18 +++++++ src/frontends/lean/old_elaborator.cpp | 1 + src/frontends/lean/util.cpp | 4 ++ src/frontends/lean/util.h | 4 ++ 10 files changed, 111 insertions(+), 67 deletions(-) create mode 100644 src/frontends/lean/match_expr.cpp create mode 100644 src/frontends/lean/match_expr.h diff --git a/src/frontends/lean/CMakeLists.txt b/src/frontends/lean/CMakeLists.txt index 87db5ee2f7..7730b09411 100644 --- a/src/frontends/lean/CMakeLists.txt +++ b/src/frontends/lean/CMakeLists.txt @@ -10,6 +10,7 @@ type_util.cpp local_ref_info.cpp decl_attributes.cpp nested_declaration.cpp opt_cmd.cpp prenum.cpp print_cmd.cpp elaborator.cpp pattern_attribute.cpp +match_expr.cpp # LEGACY old_elaborator.cpp old_attributes.cpp diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index 7d020b9307..9117f7ad51 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -31,6 +31,7 @@ Author: Leonardo de Moura #include "frontends/lean/info_annotation.h" #include "frontends/lean/structure_cmd.h" #include "frontends/lean/nested_declaration.h" +#include "frontends/lean/match_expr.h" #ifndef LEAN_DEFAULT_PARSER_CHECKPOINT_HAVE #define LEAN_DEFAULT_PARSER_CHECKPOINT_HAVE true diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index a57cc85e93..d084ebe676 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/src/frontends/lean/decl_cmds.cpp @@ -455,10 +455,6 @@ static bool is_curr_with_or_comma_or_bar(parser & p) { << n << "' in the left-hand-side does not correspond to function(s) being defined", p); } -static bool is_eqn_prefix(parser & p, bool bar_only = false) { - return p.curr_is_token(get_bar_tk()) || (!bar_only && p.curr_is_token(get_comma_tk())); -} - static void check_eqn_prefix(parser & p) { if (!is_eqn_prefix(p)) throw parser_error("invalid declaration, ',' or '|' expected", p.pos()); @@ -594,55 +590,6 @@ expr parse_local_equations(parser & p, expr const & fn) { return p.save_pos(mk_equations(fns.size(), eqns.size(), eqns.data()), pos); } -static name * g_match_name = nullptr; - -bool is_match_binder_name(name const & n) { return n == *g_match_name; } - -/** \brief Use equations compiler infrastructure to implement match-with */ -expr parse_match(parser & p, unsigned, expr const *, pos_info const & pos) { - parser::local_scope scope(p); - buffer eqns; - expr t; - try { - t = p.parse_expr(); - p.check_token_next(get_with_tk(), "invalid 'match' expression, 'with' expected"); - expr fn = mk_local(mk_fresh_name(), *g_match_name, mk_expr_placeholder(), binder_info()); - if (p.curr_is_token(get_end_tk())) { - p.next(); - // empty match-with - eqns.push_back(Fun(fn, mk_no_equation())); - expr f = p.save_pos(mk_equations(1, eqns.size(), eqns.data()), pos); - return p.mk_app(f, t, pos); - } - if (is_eqn_prefix(p)) - p.next(); // optional '|' in the first case - while (true) { - buffer locals; - auto lhs_pos = p.pos(); - expr lhs = p.parse_pattern(locals); - lhs = p.mk_app(fn, lhs, lhs_pos); - auto assign_pos = p.pos(); - p.check_token_next(get_assign_tk(), "invalid 'match' expression, ':=' expected"); - { - parser::local_scope scope2(p); - for (expr const & local : locals) - p.add_local(local); - expr rhs = p.parse_expr(); - eqns.push_back(Fun(fn, Fun(locals, p.save_pos(mk_equation(lhs, rhs), assign_pos), p))); - } - if (!is_eqn_prefix(p)) - break; - p.next(); - } - } catch (exception & ex) { - consume_until_end(p); - ex.rethrow(); - } - p.check_token_next(get_end_tk(), "invalid 'match' expression, 'end' expected"); - expr f = p.save_pos(mk_equations(1, eqns.size(), eqns.data()), pos); - return p.mk_app(f, t, pos); -} - // An Lean example is not really a definition, but we use the definition infrastructure to simulate it. enum def_cmd_kind { Theorem, Definition, MetaDefinition, Example, Abbreviation, LocalAbbreviation }; @@ -1435,9 +1382,7 @@ void register_decl_cmds(cmd_table & r) { } void initialize_decl_cmds() { - g_match_name = new name("_match"); } void finalize_decl_cmds() { - delete g_match_name; } } diff --git a/src/frontends/lean/decl_cmds.h b/src/frontends/lean/decl_cmds.h index c0103c588f..27a0ee3a8a 100644 --- a/src/frontends/lean/decl_cmds.h +++ b/src/frontends/lean/decl_cmds.h @@ -10,23 +10,18 @@ Author: Leonardo de Moura #include "frontends/lean/cmd_table.h" namespace lean { class parser; -/** - \brief Parse (optional) universe parameters '.{' l_1 ... l_k '}' +/** \brief Parse (optional) universe parameters '.{' l_1 ... l_k '}' Store the result in \c ps. - Return true when levels were provided. -*/ + + Return true when levels were provided. */ bool parse_univ_params(parser & p, buffer & ps); -void validate_match_pattern(parser const & p, expr const & lhs, buffer const & locals); -expr parse_match_pattern(parser & p, buffer & locals); -expr parse_match(parser & p, unsigned, expr const *, pos_info const & pos); + expr parse_local_equations(parser & p, expr const & fn); -/** \brief Return true iff \c n is the auxiliary name used to elaborate match-expressions. */ -bool is_match_binder_name(name const & n); +/** \brief Add universe levels from \c found_ls to \c ls_buffer + (only the levels that do not already occur in \c ls_buffer are added). -/** \brief Add universe levels from \c found_ls to \c ls_buffer (only the levels that do not already occur in \c ls_buffer are added). - Then sort \c ls_buffer (using the order in which the universe levels were declared). -*/ + Then sort \c ls_buffer (using the order in which the universe levels were declared). */ void update_univ_parameters(buffer & ls_buffer, name_set const & found_ls, parser const & p); /** \brief Parse a local abbreviation command */ diff --git a/src/frontends/lean/init_module.cpp b/src/frontends/lean/init_module.cpp index 483d00215b..2471c8e800 100644 --- a/src/frontends/lean/init_module.cpp +++ b/src/frontends/lean/init_module.cpp @@ -28,6 +28,7 @@ Author: Leonardo de Moura #include "frontends/lean/prenum.h" #include "frontends/lean/old_attributes.h" #include "frontends/lean/elaborator.h" +#include "frontends/lean/match_expr.h" namespace lean { void initialize_frontend_lean_module() { @@ -54,10 +55,12 @@ void initialize_frontend_lean_module() { initialize_local_ref_info(); initialize_decl_cmds(); initialize_nested_declaration(); + initialize_match_expr(); initialize_elaborator(); } void finalize_frontend_lean_module() { finalize_elaborator(); + finalize_match_expr(); finalize_old_attributes(); finalize_nested_declaration(); finalize_decl_cmds(); diff --git a/src/frontends/lean/match_expr.cpp b/src/frontends/lean/match_expr.cpp new file mode 100644 index 0000000000..4438ae8512 --- /dev/null +++ b/src/frontends/lean/match_expr.cpp @@ -0,0 +1,72 @@ +/* +Copyright (c) 2016 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "util/fresh_name.h" +#include "kernel/abstract.h" +#include "library/placeholder.h" +#include "library/definitional/equations.h" +#include "frontends/lean/tokens.h" +#include "frontends/lean/util.h" +#include "frontends/lean/parser.h" + +namespace lean { +static name * g_match_name = nullptr; + +bool is_match_binder_name(name const & n) { return n == *g_match_name; } + +/** \brief Use equations compiler infrastructure to implement match-with */ +expr parse_match(parser & p, unsigned, expr const *, pos_info const & pos) { + parser::local_scope scope(p); + buffer eqns; + expr t; + try { + t = p.parse_expr(); + p.check_token_next(get_with_tk(), "invalid 'match' expression, 'with' expected"); + expr fn = mk_local(mk_fresh_name(), *g_match_name, mk_expr_placeholder(), binder_info()); + if (p.curr_is_token(get_end_tk())) { + p.next(); + // empty match-with + eqns.push_back(Fun(fn, mk_no_equation())); + expr f = p.save_pos(mk_equations(1, eqns.size(), eqns.data()), pos); + return p.mk_app(f, t, pos); + } + if (is_eqn_prefix(p)) + p.next(); // optional '|' in the first case + while (true) { + buffer locals; + auto lhs_pos = p.pos(); + expr lhs = p.parse_pattern(locals); + lhs = p.mk_app(fn, lhs, lhs_pos); + auto assign_pos = p.pos(); + p.check_token_next(get_assign_tk(), "invalid 'match' expression, ':=' expected"); + { + parser::local_scope scope2(p); + for (expr const & local : locals) + p.add_local(local); + expr rhs = p.parse_expr(); + eqns.push_back(Fun(fn, Fun(locals, p.save_pos(mk_equation(lhs, rhs), assign_pos), p))); + } + if (!is_eqn_prefix(p)) + break; + p.next(); + } + } catch (exception & ex) { + consume_until_end(p); + ex.rethrow(); + } + p.check_token_next(get_end_tk(), "invalid 'match' expression, 'end' expected"); + expr f = p.save_pos(mk_equations(1, eqns.size(), eqns.data()), pos); + return p.mk_app(f, t, pos); +} + +void initialize_match_expr() { + g_match_name = new name("_match"); +} + +void finalize_match_expr() { + delete g_match_name; +} +} diff --git a/src/frontends/lean/match_expr.h b/src/frontends/lean/match_expr.h new file mode 100644 index 0000000000..fc3d2301af --- /dev/null +++ b/src/frontends/lean/match_expr.h @@ -0,0 +1,18 @@ +/* +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "frontends/lean/util.h" +namespace lean { +class parser; +/** \brief Return true iff \c n is the auxiliary name used to elaborate match-expressions. */ +bool is_match_binder_name(name const & n); + +expr parse_match(parser & p, unsigned, expr const *, pos_info const & pos); + +void initialize_match_expr(); +void finalize_match_expr(); +} diff --git a/src/frontends/lean/old_elaborator.cpp b/src/frontends/lean/old_elaborator.cpp index fb5de7344f..025eb7c5b5 100644 --- a/src/frontends/lean/old_elaborator.cpp +++ b/src/frontends/lean/old_elaborator.cpp @@ -55,6 +55,7 @@ Author: Leonardo de Moura #include "frontends/lean/info_manager.h" #include "frontends/lean/info_annotation.h" #include "frontends/lean/old_elaborator.h" +#include "frontends/lean/match_expr.h" // #include "frontends/lean/info_tactic.h" // #include "frontends/lean/begin_end_annotation.h" #include "frontends/lean/old_elaborator_exception.h" diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp index 6421fd9829..d434ab26f4 100644 --- a/src/frontends/lean/util.cpp +++ b/src/frontends/lean/util.cpp @@ -70,6 +70,10 @@ name remove_root_prefix(name const & n) { return n.replace_prefix(get_root_tk(), name()); } +bool is_eqn_prefix(parser & p, bool bar_only = false) { + return p.curr_is_token(get_bar_tk()) || (!bar_only && p.curr_is_token(get_comma_tk())); +} + // Sort local names by order of occurrence, and copy the associated parameters to ps void sort_locals(buffer const & locals, parser const & p, buffer & ps) { for (expr const & l : locals) { diff --git a/src/frontends/lean/util.h b/src/frontends/lean/util.h index 7f50b79347..5a8fdf6348 100644 --- a/src/frontends/lean/util.h +++ b/src/frontends/lean/util.h @@ -27,6 +27,10 @@ void check_atomic(name const & n); void check_in_section(parser const & p); bool is_root_namespace(name const & n); name remove_root_prefix(name const & n); + +/** \brief Return true iff the next token is the prefix of a pattern-matching equation */ +bool is_eqn_prefix(parser & p, bool bar_only = false); + /** \brief Return the local levels in \c ls that are not tagged as variables. A local level is tagged as variable if it associated with a variable. */