refactor(frontends/lean): move match-expr parser to different module

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

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

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<expr> 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<expr> 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;
 }
 }

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 <tt>'.{' l_1 ... l_k '}'</tt>
+/** \brief Parse (optional) universe parameters <tt>'.{' l_1 ... l_k '}'</tt>
     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<name> & ps);
-void validate_match_pattern(parser const & p, expr const & lhs, buffer<expr> const & locals);
-expr parse_match_pattern(parser & p, buffer<expr> & 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<name> & ls_buffer, name_set const & found_ls, parser const & p);
 
 /** \brief Parse a local abbreviation command */

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();

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<expr> 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<expr> 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;
+}
+}

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();
+}

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"

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<expr> const & locals, parser const & p, buffer<expr> & ps) {
     for (expr const & l : locals) {

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.
 */