feag(frontends/lean): explicit delimiters in declaration parameters

Comment from parser.h

This commit makes sure that all declaration parameters must be surrounded with some kind of bracket. (e.g., '()', '{}', '[]').
The goal is to avoid counter-intuitive declarations such as:

              example p : false := trivial
              def main proof : false := trivial

which would be parsed as

              example (p : false) : _ := trivial

              def main (proof : false) : _ := trivial

where `_` in both cases is elaborated into `true`. This issue was raised by @gebner in the slack channel.

Remark: we still want implicit delimiters for lambda/pi expressions. That is, we want to write

               fun x : t, s
           or
               fun x, s

instead of

               fun (x : t), s

src/frontends/lean/decl_util.cpp

@@ -60,7 +60,7 @@ expr parse_single_header(parser & p, declaration_name_scope & scope, buffer <nam
             scope.set_name(c_name);
         }
     }
-    p.parse_optional_binders(params, /* allow_default */ true);
+    p.parse_optional_binders(params, /* allow_default */ true, /* explicit delimiters */ true);
     for (expr const & param : params)
         p.add_local(param);
     expr type;
@@ -106,7 +106,7 @@ void parse_mutual_header(parser & p, buffer <name> & lp_names, buffer <expr> & c
     if (cs.size() < 2) {
         throw parser_error("invalid mutual declaration, must provide more than one identifier (separated by commas)", p.pos());
     }
-    p.parse_optional_binders(params, /* allow_default */ true);
+    p.parse_optional_binders(params, /* allow_default */ true, /* explicit delimiters */ true);
     for (expr const & param : params)
         p.add_local(param);
     for (expr const & c : cs)

src/frontends/lean/parser.cpp

@@ -1053,6 +1053,10 @@ void parser::parse_binders_core(buffer<expr> & r, parse_binders_config & cfg) {
     bool first = true;
     while (true) {
         if (curr_is_identifier() || curr_is_token(get_placeholder_tk())) {
+            if (cfg.m_explicit_delimiters) {
+                throw parser_error("invalid binder declaration, delimiter/bracket expected (i.e., '(', '{', '[', '{{')",
+                                   pos());
+            }
             /* We only allow the default parameter value syntax for declarations with
                surrounded by () */
             bool new_allow_default = false;

src/frontends/lean/parser.h

@@ -129,6 +129,34 @@ class parser : public abstract_parser {
         /* (input) If true, it will allow binders of the form (x : T := v), and they will be converted
            into (x : opt_param T v) */
         bool     m_allow_default{false};
+        /* (input) If true, then all binders must be surrounded with some kind of bracket. (e.g., '()', '{}', '[]').
+           We use this feature when parsing examples/definitions/theorems. The goal is to avoid counter-intuitive
+           declarations such as:
+
+              example p : false := trivial
+              def main proof : false := trivial
+
+           which would be parsed as
+
+              example (p : false) : _ := trivial
+
+              def main (proof : false) : _ := trivial
+
+           where `_` in both cases is elaborated into `true`. This issue was raised by @gebner in the slack channel.
+
+
+           Remark: we still want implicit delimiters for lambda/pi expressions. That is, we want to
+           write
+
+               fun x : t, s
+           or
+               fun x, s
+
+           instead of
+
+               fun (x : t), s
+        */
+        bool     m_explicit_delimiters{false};
         /* (input and output)
           If m_infer_kind != nullptr, then a sequence of binders can be prefixed with '{}' or '()'
           Moreover, *m_infer_kind will be updated with
@@ -343,10 +371,11 @@ public:
         parse_binders(r, cfg);
     }
 
-    local_environment parse_optional_binders(buffer<expr> & r, bool allow_default = false) {
+    local_environment parse_optional_binders(buffer<expr> & r, bool allow_default = false, bool explicit_delimiters = false) {
         parse_binders_config cfg;
-        cfg.m_allow_empty   = true;
-        cfg.m_allow_default = allow_default;
+        cfg.m_allow_empty         = true;
+        cfg.m_allow_default       = allow_default;
+        cfg.m_explicit_delimiters = explicit_delimiters;
         return parse_binders(r, cfg);
     }
 

tests/lean/1293.lean

@@ -10,6 +10,6 @@ example : true := by unify (var 0) (var 0) >> return ()
 
 example : true := by is_def_eq (var 0) (var 0) >> return ()
 
-example foo trivial := by do
+example (foo trivial) := by do
 t ← infer_type (var 0),
 to_expr ``(trivial) >>= apply

tests/lean/1293.lean.expected.out

@@ -13,15 +13,15 @@ state:
 1293.lean:11:21: error: tactic 'is_def_eq' failed, given expression should not contain de-Bruijn variables, they should be replaced with local constants before using this tactic
 state:
 ⊢ true
-1293.lean:13:26: error: tactic 'infer_type' failed, given expression should not contain de-Bruijn variables, they should be replaced with local constants before using this tactic
+1293.lean:13:28: error: tactic 'infer_type' failed, given expression should not contain de-Bruijn variables, they should be replaced with local constants before using this tactic
 state:
 foo : ?m_1,
 trivial : ?m_2
 ⊢ ?m_3
-1293.lean:13:8: error: don't know how to synthesize placeholder
+1293.lean:13:9: error: don't know how to synthesize placeholder
 context:
 ⊢ Sort ?
-1293.lean:13:12: error: don't know how to synthesize placeholder
+1293.lean:13:13: error: don't know how to synthesize placeholder
 context:
 foo : ⁇
 ⊢ Sort ?

tests/lean/explicit_delimiters.lean

@@ -0,0 +1,9 @@
+example p : false := trivial -- Error
+
+def main proof : false := trivial -- Error
+
+example (p : false) := trivial
+
+def main' (proof : false) := trivial
+
+example := trivial

tests/lean/explicit_delimiters.lean.expected.out

@@ -0,0 +1,2 @@
+explicit_delimiters.lean:1:8: error: invalid binder declaration, delimiter/bracket expected (i.e., '(', '{', '[', '{{')
+explicit_delimiters.lean:3:9: error: invalid binder declaration, delimiter/bracket expected (i.e., '(', '{', '[', '{{')

tests/lean/param.lean

@@ -1,9 +1,9 @@
 --
-definition foo1 a b c := a + b + (c:nat)
+definition foo1 (a b c) := a + b + (c:nat)
 
-definition foo2 (a : nat) b c := a + b + c
+definition foo2 (a : nat) (b c) := a + b + c
 
-definition foo3 a b (c : nat) := a + b + c
+definition foo3 (a b) (c : nat) := a + b + c
 
 definition foo4 (a b c : nat) := a + b + c
 
@@ -17,4 +17,4 @@ definition foo8 (a b c : nat) : nat := a + b + c
 
 definition foo9 (a : nat) (b : nat) (c : nat) : nat := a + b + c
 
-definition foo10 (a : nat) b (c : nat) : nat := a + b + c
+definition foo10 (a : nat) (b) (c : nat) : nat := a + b + c

tests/lean/run/1813.lean

@@ -1,6 +1,6 @@
 open tactic
 
-example {A B : Type} (f : A -> B) a b c (h1 : f a = b) (h2 : f a = c) : false :=
+example {A B : Type} (f : A -> B) (a b c) (h1 : f a = b) (h2 : f a = c) : false :=
 begin
   rw h1 at *,
   guard_hyp h1 := f a = b,
@@ -8,7 +8,7 @@ begin
   admit
 end
 
-example {A B : Type} (f : A -> B) a b c (h1 : f a = b) (h2 : f a = c) : false :=
+example {A B : Type} (f : A -> B) (a b c) (h1 : f a = b) (h2 : f a = c) : false :=
 begin
   rw [id h1] at *,
   guard_hyp h1 := f a = b,
@@ -16,7 +16,7 @@ begin
   admit
 end
 
-example {A B : Type} (f : A -> B) a b c (h1 : f a = b) (h2 : f a = c) : false :=
+example {A B : Type} (f : A -> B) (a b c) (h1 : f a = b) (h2 : f a = c) : false :=
 begin
   rw [id id h1] at *,
   guard_hyp h1 := f a = b,

tests/lean/run/662.lean

@@ -20,7 +20,7 @@ end var
 
 open term
 
-definition Term t := Π (var : type → Type), @term var t
+definition Term (t) := Π (var : type → Type), @term var t
 open unit
 
 definition count_vars : Π {t : type}, @term (λ x, unit) t -> nat

tests/lean/run/level_bug3.lean

@@ -1,6 +1,6 @@
 variables {a r : Type}
 
-definition f a := Πr, (a -> r) -> r
+definition f (a) := Πr, (a -> r) -> r
 
 lemma blah2 (sa : f a) (k : (a -> r)) :
   sa r k = sa r k :=

tests/lean/run/nested_common_subexpr_issue.lean

@@ -4,7 +4,7 @@ def fib_aux : ℕ → ℕ × ℕ
 | 0     := (0, 1)
 | (n+1) := let p := fib_aux n in (p.2, p.1 + p.2)
 
-def fib n := (fib_aux n).2
+def fib (n) := (fib_aux n).2
 
 #eval fib 10000
 
@@ -12,6 +12,6 @@ def fib_aux2 : ℕ → ℕ × ℕ
 | 0     := (0, 1)
 | (n+1) := let (a, b) := fib_aux2 n in (b, a + b)
 
-def fib2 n := (fib_aux2 n).2
+def fib2 (n) := (fib_aux2 n).2
 
 #eval fib2 10000

tests/lean/run/quote_bas.lean

@@ -68,11 +68,11 @@ Quote.quote l n r
 @[simp] lemma eval_quote {V : Type u} {l : Env V} (n : nat) {V' : Type v} {r : Env V'} [Quote l n r] : evalExpr (merge l r) (quote n) = n :=
 Quote.eval_quote l n r
 
-instance quote_one V (v : Env V) : Quote v 1 novars :=
+instance quote_one (V) (v : Env V) : Quote v 1 novars :=
 { quote      := One,
   eval_quote := rfl }
 
-instance quote_mul {V : Type u} (v : Env V) n {V' : Type v} (v' : Env V') m {V'' : Type w} (v'' : Env V'')
+instance quote_mul {V : Type u} (v : Env V) (n) {V' : Type v} (v' : Env V') (m) {V'' : Type w} (v'' : Env V'')
                    [Quote v n v'] [Quote (merge v v') m v''] :
                    Quote v (n * m) (merge v' v'') :=
 { quote      := Mult (map_var sum_assoc (map_var inl (quote n))) (map_var sum_assoc (quote m)),

tests/lean/run/soundness.lean

@@ -30,12 +30,12 @@ namespace PropF
   local infixr `⇒`:27    := Impl
   notation `⊥`           := Bot
 
-  def Neg A       := A ⇒ ⊥
-  notation ~ A    := Neg A
-  def Top         := ~⊥
-  notation `⊤`    := Top
-  def BiImpl A B  := A ⇒ B ∧ B ⇒ A
-  infixr `⇔`:27   := BiImpl
+  def Neg (A)      := A ⇒ ⊥
+  notation ~ A     := Neg A
+  def Top          := ~⊥
+  notation `⊤`     := Top
+  def BiImpl (A B) := A ⇒ B ∧ B ⇒ A
+  infixr `⇔`:27    := BiImpl
 
   def valuation   := PropVar → bool
 
@@ -51,12 +51,12 @@ namespace PropF
 
   -- the valuation v satisfies a list of PropF, if forall (A : PropF) in Γ,
   -- (TrueQ v A) is tt (the Boolean true)
-  def Satisfies v (Γ : list PropF) := ∀ A, A ∈ Γ → is_true (TrueQ v A)
-  def Models Γ A                   := ∀ v, Satisfies v Γ → is_true (TrueQ v A)
+  def Satisfies (v) (Γ : list PropF) := ∀ A, A ∈ Γ → is_true (TrueQ v A)
+  def Models (Γ A)                   := ∀ v, Satisfies v Γ → is_true (TrueQ v A)
 
   infix `⊨`:80 := Models
 
-  def Valid p := [] ⊨ p
+  def Valid (p) := [] ⊨ p
   reserve infix ` ⊢ `:26
 
   /- Provability -/
@@ -76,7 +76,7 @@ namespace PropF
 
   infix ⊢ := Nc
 
-  def Provable A := [] ⊢ A
+  def Provable (A) := [] ⊢ A
 
   def Prop_Soundness := ∀ A, Provable A → Valid A