chore(frontends/lean): reduce code duplication

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/frontends/lean/decl_cmds.cpp

@@ -18,12 +18,7 @@ Author: Leonardo de Moura
 
 namespace lean {
 static name g_llevel_curly(".{");
-static name g_lcurly("{");
 static name g_rcurly("}");
-static name g_ldcurly("⦃");
-static name g_rdcurly("⦄");
-static name g_lbracket("[");
-static name g_rbracket("]");
 static name g_colon(":");
 static name g_assign(":=");
 static name g_private("[private]");
@@ -45,44 +40,6 @@ environment universe_cmd(parser & p) {
     return env;
 }
 
-binder_info parse_open_binder_info(parser & p) {
-    if (p.curr_is_token(g_lcurly)) {
-        check_in_section(p);
-        p.next();
-        if (p.curr_is_token(g_lcurly)) {
-            p.next();
-            return mk_strict_implicit_binder_info();
-        } else {
-            return mk_implicit_binder_info();
-        }
-    } else if (p.curr_is_token(g_lbracket)) {
-        check_in_section(p);
-        p.next();
-        return mk_cast_binder_info();
-    } else if (p.curr_is_token(g_ldcurly)) {
-        check_in_section(p);
-        p.next();
-        return mk_strict_implicit_binder_info();
-    } else {
-        return binder_info();
-    }
-}
-
-void parse_close_binder_info(parser & p, binder_info const & bi) {
-    if (bi.is_implicit()) {
-        p.check_token_next(g_rcurly, "invalid declaration, '}' expected");
-    } else if (bi.is_cast()) {
-        p.check_token_next(g_rbracket, "invalid declaration, ']' expected");
-    } else if (bi.is_strict_implicit()) {
-        if (p.curr_is_token(g_lcurly)) {
-            p.next();
-            p.check_token_next(g_rdcurly, "invalid declaration, '}' expected");
-        } else {
-            p.check_token_next(g_rdcurly, "invalid declaration, '⦄' expected");
-        }
-    }
-}
-
 bool parse_univ_params(parser & p, buffer<name> & ps) {
     if (p.curr_is_token(g_llevel_curly)) {
         p.next();
@@ -111,7 +68,9 @@ void update_univ_parameters(buffer<name> & ls_buffer, name_set const & found, pa
 
 static environment declare_var(parser & p, environment env,
                                name const & n, level_param_names const & ls, expr const & type,
-                               bool is_axiom, binder_info const & bi, pos_info const & pos) {
+                               bool is_axiom, optional<binder_info> const & _bi, pos_info const & pos) {
+    binder_info bi;
+    if (_bi) bi = *_bi;
     if (in_section(p.env())) {
         p.add_local(p.save_pos(mk_local(n, type, bi), pos));
         return env;
@@ -128,9 +87,16 @@ static environment declare_var(parser & p, environment env,
     }
 }
 
+optional<binder_info> parse_binder_info(parser & p) {
+    optional<binder_info> bi = p.parse_optional_binder_info();
+    if (bi)
+        check_in_section(p);
+    return bi;
+}
+
 environment variable_cmd_core(parser & p, bool is_axiom) {
     auto pos = p.pos();
-    binder_info bi = parse_open_binder_info(p);
+    optional<binder_info> bi = parse_binder_info(p);
     name n = p.check_id_next("invalid declaration, identifier expected");
     check_atomic(n);
     buffer<name> ls_buffer;
@@ -152,7 +118,7 @@ environment variable_cmd_core(parser & p, bool is_axiom) {
         p.next();
         type = p.parse_expr();
     }
-    parse_close_binder_info(p, bi);
+    p.parse_close_binder_info(bi);
     level_param_names ls;
     if (in_section(p.env())) {
         ls = to_level_param_names(collect_univ_params(type));
@@ -308,7 +274,7 @@ environment theorem_cmd(parser & p) {
 static environment variables_cmd(parser & p) {
     auto pos = p.pos();
     buffer<name> ids;
-    binder_info bi = parse_open_binder_info(p);
+    optional<binder_info> bi = parse_binder_info(p);
     while (!p.curr_is_token(g_colon)) {
         name id = p.check_id_next("invalid parameters declaration, identifier expected");
         check_atomic(id);
@@ -320,7 +286,7 @@ static environment variables_cmd(parser & p) {
         scope1.emplace(p);
     parser::param_universe_scope scope2(p);
     expr type = p.parse_expr();
-    parse_close_binder_info(p, bi);
+    p.parse_close_binder_info(bi);
     level_param_names ls = to_level_param_names(collect_univ_params(type));
     type = p.elaborate(type);
     environment env = p.env();

src/frontends/lean/parser.cpp

@@ -538,6 +538,82 @@ std::pair<expr, expr> parser::elaborate(name const & n, expr const & t, expr con
     return ::lean::elaborate(m_env, m_ios, n, t, v, m_hints, &pp);
 }
 
+[[ noreturn ]] void throw_invalid_open_binder(pos_info const & pos) {
+    throw parser_error("invalid binder, '(', '{', '[', '{{', '⦃' or identifier expected", pos);
+}
+
+/**
+   \brief Return an optional binder_info object based on the current token
+      - '('           : default
+      - '{'          : implicit
+      - '{{' or '⦃'  : strict implicit
+      - '['          : cast
+*/
+optional<binder_info> parser::parse_optional_binder_info() {
+    if (curr_is_token(g_lparen)) {
+        next();
+        return some(binder_info());
+    } else if (curr_is_token(g_lcurly)) {
+        next();
+        if (curr_is_token(g_lcurly)) {
+            next();
+            return some(mk_strict_implicit_binder_info());
+        } else {
+            return some(mk_implicit_binder_info());
+        }
+    } else if (curr_is_token(g_lbracket)) {
+        next();
+        return some(mk_cast_binder_info());
+    } else if (curr_is_token(g_ldcurly)) {
+        next();
+        return some(mk_strict_implicit_binder_info());
+    } else {
+        return optional<binder_info>();
+    }
+}
+
+/**
+   \brief Return binder_info object based on the current token, it fails if the current token
+   is not '(', '{', '{{', '⦃', or '['
+
+   \see parse_optional_binder_info
+*/
+binder_info parser::parse_binder_info() {
+    auto p = pos();
+    if (auto bi = parse_optional_binder_info()) {
+        return *bi;
+    } else {
+        throw_invalid_open_binder(p);
+    }
+}
+
+/**
+   \brief Consume the next token based on the value of \c bi
+     - none            : do not consume anything
+     - default         : consume ')'
+     - implicit        : consume '}'
+     - strict implicit : consume '}}' or '⦄'
+     - cast            : consume ']'
+*/
+void parser::parse_close_binder_info(optional<binder_info> const & bi) {
+    if (!bi) {
+        return;
+    } else if (bi->is_implicit()) {
+        check_token_next(g_rcurly, "invalid declaration, '}' expected");
+    } else if (bi->is_cast()) {
+        check_token_next(g_rbracket, "invalid declaration, ']' expected");
+    } else if (bi->is_strict_implicit()) {
+        if (curr_is_token(g_rcurly)) {
+            next();
+            check_token_next(g_rcurly, "invalid declaration, '}' expected");
+        } else {
+            check_token_next(g_rdcurly, "invalid declaration, '⦄' expected");
+        }
+    } else {
+        check_token_next(g_rparen, "invalid declaration, ')' expected");
+    }
+}
+
 /** \brief Parse <tt>ID ':' expr</tt>, where the expression represents the type of the identifier. */
 expr parser::parse_binder_core(binder_info const & bi) {
     auto p  = pos();
@@ -558,36 +634,11 @@ expr parser::parse_binder_core(binder_info const & bi) {
 expr parser::parse_binder() {
     if (curr_is_identifier()) {
         return parse_binder_core(binder_info());
-    } else if (curr_is_token(g_lparen)) {
-        next();
-        auto p = parse_binder_core(binder_info());
-        check_token_next(g_rparen, "invalid binder, ')' expected");
-        return p;
-    } else if (curr_is_token(g_lcurly)) {
-        next();
-        if (curr_is_token(g_lcurly)) {
-            next();
-            auto p = parse_binder_core(mk_strict_implicit_binder_info());
-            check_token_next(g_rcurly, "invalid binder, '}' expected");
-            check_token_next(g_rcurly, "invalid binder, '}' expected");
-            return p;
-        } else {
-            auto p = parse_binder_core(mk_implicit_binder_info());
-            check_token_next(g_rcurly, "invalid binder, '}' expected");
-            return p;
-        }
-    } else if (curr_is_token(g_lbracket)) {
-        next();
-        auto p = parse_binder_core(mk_cast_binder_info());
-        check_token_next(g_rbracket, "invalid binder, ']' expected");
-        return p;
-    } else if (curr_is_token(g_ldcurly)) {
-        next();
-        auto p = parse_binder_core(mk_strict_implicit_binder_info());
-        check_token_next(g_rdcurly, "invalid binder, '⦄' expected");
-        return p;
     } else {
-        throw parser_error("invalid binder, '(', '{', '[', '{{', '⦃' or identifier expected", pos());
+        binder_info bi = parse_binder_info();
+        auto r = parse_binder_core(bi);
+        parse_close_binder_info(bi);
+        return r;
     }
 }
 
@@ -614,36 +665,20 @@ void parser::parse_binder_block(buffer<expr> & r, binder_info const & bi) {
 }
 
 void parser::parse_binders_core(buffer<expr> & r) {
-    if (curr_is_identifier()) {
+    while (true) {
-        parse_binder_block(r, binder_info());
+        if (curr_is_identifier()) {
-    } else if (curr_is_token(g_lparen)) {
-        next();
-        if (!parse_local_notation_decl())
             parse_binder_block(r, binder_info());
-        check_token_next(g_rparen, "invalid binder, ')' expected");
-    } else if (curr_is_token(g_lcurly)) {
-        next();
-        if (curr_is_token(g_lcurly)) {
-            next();
-            parse_binder_block(r, mk_strict_implicit_binder_info());
-            check_token_next(g_rcurly, "invalid binder, '}' expected");
-            check_token_next(g_rcurly, "invalid binder, '}' expected");
         } else {
-            parse_binder_block(r, mk_implicit_binder_info());
+            optional<binder_info> bi = parse_optional_binder_info();
-            check_token_next(g_rcurly, "invalid binder, '}' expected");
+            if (bi) {
+                if (!parse_local_notation_decl())
+                    parse_binder_block(r, *bi);
+                parse_close_binder_info(bi);
+            } else {
+                return;
+            }
         }
-    } else if (curr_is_token(g_lbracket)) {
-        next();
-        parse_binder_block(r, mk_cast_binder_info());
-        check_token_next(g_rbracket, "invalid binder, ']' expected");
-    } else if (curr_is_token(g_ldcurly)) {
-        next();
-        parse_binder_block(r, mk_strict_implicit_binder_info());
-        check_token_next(g_rdcurly, "invalid binder, '⦄' expected");
-    } else {
-        return;
     }
-    parse_binders_core(r);
 }
 
 local_environment parser::parse_binders(buffer<expr> & r) {
@@ -652,7 +687,7 @@ local_environment parser::parse_binders(buffer<expr> & r) {
     unsigned old_sz = r.size();
     parse_binders_core(r);
     if (old_sz == r.size())
-        throw parser_error("invalid binder, '(', '{', '[', '{{', '⦃' or identifier expected", pos());
+        throw_invalid_open_binder(pos());
     return local_environment(m_env);
 }
 

src/frontends/lean/parser.h

@@ -205,6 +205,10 @@ public:
 
     expr parse_binder();
     local_environment parse_binders(buffer<expr> & r);
+    optional<binder_info> parse_optional_binder_info();
+    binder_info parse_binder_info();
+    void parse_close_binder_info(optional<binder_info> const & bi);
+    void parse_close_binder_info(binder_info const & bi) { return parse_close_binder_info(optional<binder_info>(bi)); }
 
     /** \brief Convert an identifier into an expression (constant or local constant) based on the current scope */
     expr id_to_expr(name const & id, pos_info const & p);