feat(frontends/lean/parser): reject ambiguous parameter declaration, closes #242

src/frontends/lean/decl_cmds.cpp

@@ -329,7 +329,8 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool is_opaque, boo
         } else {
             buffer<expr> ps;
             optional<local_environment> lenv;
-            lenv = p.parse_binders(ps);
+            bool last_block_delimited = false;
+            lenv = p.parse_binders(ps, last_block_delimited);
             auto pos = p.pos();
             if (p.curr_is_token(get_colon_tk())) {
                 p.next();
@@ -342,6 +343,12 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool is_opaque, boo
                     value = p.parse_scoped_expr(ps, *lenv);
                 }
             } else {
+                if (!last_block_delimited && !ps.empty() &&
+                    !is_placeholder(mlocal_type(ps.back()))) {
+                    throw parser_error("invalid declaration, ambiguous parameter declaration, "
+                                       "(solution: put parentheses around parameters)",
+                                       pos);
+                }
                 type = p.save_pos(mk_expr_placeholder(), p.pos());
                 p.check_token_next(get_assign_tk(), "invalid declaration, ':=' expected");
                 value = p.parse_scoped_expr(ps, *lenv);

src/frontends/lean/parser.cpp

@@ -792,13 +792,16 @@ void parser::parse_binder_block(buffer<expr> & r, binder_info const & bi) {
     }
 }
 
-void parser::parse_binders_core(buffer<expr> & r, buffer<notation_entry> * nentries) {
+void parser::parse_binders_core(buffer<expr> & r, buffer<notation_entry> * nentries,
+                                bool & last_block_delimited) {
     while (true) {
         if (curr_is_identifier()) {
             parse_binder_block(r, binder_info());
+            last_block_delimited = false;
         } else {
             optional<binder_info> bi = parse_optional_binder_info();
             if (bi) {
+                last_block_delimited = true;
                 if (!parse_local_notation_decl(nentries))
                     parse_binder_block(r, *bi);
                 parse_close_binder_info(bi);
@@ -809,11 +812,12 @@ void parser::parse_binders_core(buffer<expr> & r, buffer<notation_entry> * nentr
     }
 }
 
-local_environment parser::parse_binders(buffer<expr> & r, buffer<notation_entry> * nentries) {
+local_environment parser::parse_binders(buffer<expr> & r, buffer<notation_entry> * nentries,
+                                        bool & last_block_delimited) {
     flet<environment> save(m_env, m_env); // save environment
     local_expr_decls::mk_scope scope(m_local_decls);
     unsigned old_sz = r.size();
-    parse_binders_core(r, nentries);
+    parse_binders_core(r, nentries, last_block_delimited);
     if (old_sz == r.size())
         throw_invalid_open_binder(pos());
     return local_environment(m_env);

src/frontends/lean/parser.h

@@ -179,8 +179,8 @@ class parser {
     expr parse_string_expr();
     expr parse_binder_core(binder_info const & bi);
     void parse_binder_block(buffer<expr> & r, binder_info const & bi);
-    void parse_binders_core(buffer<expr> & r, buffer<notation_entry> * nentries);
-    local_environment parse_binders(buffer<expr> & r, buffer<notation_entry> * nentries);
+    void parse_binders_core(buffer<expr> & r, buffer<notation_entry> * nentries, bool & last_block_delimited);
+    local_environment parse_binders(buffer<expr> & r, buffer<notation_entry> * nentries, bool & last_block_delimited);
     bool parse_local_notation_decl(buffer<notation_entry> * entries);
 
     friend environment section_cmd(parser & p);
@@ -310,8 +310,15 @@ public:
     level parse_level(unsigned rbp = 0);
 
     expr parse_binder();
-    local_environment parse_binders(buffer<expr> & r) { return parse_binders(r, nullptr); }
-    local_environment parse_binders(buffer<expr> & r, buffer<notation_entry> & nentries) { return parse_binders(r, &nentries); }
+    local_environment parse_binders(buffer<expr> & r, bool & last_block_delimited) {
+        return parse_binders(r, nullptr, last_block_delimited);
+    }
+    local_environment parse_binders(buffer<expr> & r) {
+        bool tmp; return parse_binders(r, nullptr, tmp);
+    }
+    local_environment parse_binders(buffer<expr> & r, buffer<notation_entry> & nentries) {
+        bool tmp; return parse_binders(r, &nentries, tmp);
+    }
     optional<binder_info> parse_optional_binder_info();
     binder_info parse_binder_info();
     void parse_close_binder_info(optional<binder_info> const & bi);

tests/lean/param.lean

@@ -0,0 +1,22 @@
+import data.num
+open num
+
+definition foo1 a b c := a + b + c
+
+definition foo2 (a : num) b c := a + b + c
+
+definition foo3 a b (c : num) := a + b + c
+
+definition foo4 (a b c : num) := a + b + c
+
+definition foo5 (a b c) : num := a + b + c
+
+definition foo6 {a b c} : num := a + b + c
+
+definition foo7 a b c : num := a + b + c  -- Error
+
+definition foo8 (a b c : num) : num := a + b + c
+
+definition foo9 (a : num) (b : num) (c : num) : num := a + b + c
+
+definition foo10 (a : num) b (c : num) : num := a + b + c

tests/lean/param.lean.expected.out

@@ -0,0 +1 @@
+param.lean:16:28: error: invalid declaration, ambiguous parameter declaration, (solution: put parentheses around parameters)