From 8c8cefcb0cab2d78d23c1403c5cdade03b4ef0fb Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 23 Dec 2013 21:24:50 -0800
Subject: [PATCH] feat(frontends/lean/parser): compact definitions

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/parser.cpp            | 21 +++++++++++++--------
 tests/lean/compact_def.lean              |  4 ++++
 tests/lean/compact_def.lean.expected.out |  8 ++++++++
 3 files changed, 25 insertions(+), 8 deletions(-)
 create mode 100644 tests/lean/compact_def.lean
 create mode 100644 tests/lean/compact_def.lean.expected.out

diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 63c6363085..2868f79482 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -1178,7 +1178,7 @@ class parser::imp {
         \remark If implicit_decls is true, then we allow declarations
         with curly braces. These declarations are used to tag implicit
         arguments. Such as:
-        <code> Definition f {A : Type} (a b : A), A := ... </code>
+        <code> Definition f {A : Type} (a b : A) : A := ... </code>
 
         \see parse_simple_bindings
     */
@@ -1213,16 +1213,21 @@ class parser::imp {
         }
     }
 
-    /** \brief Parse bindings for object such as: definitions, theorems, axioms, variables ... */
-    void parse_object_bindings(bindings_buffer & result) {
-        parse_bindings(result, true, false);
-    }
-
     /** \brief Parse bindings for expressions such as: lambda, pi, forall, exists */
     void parse_expr_bindings(bindings_buffer & result) {
         parse_bindings(result, false, true);
     }
 
+    /** \brief Parse bindings for object such as: axioms, variables ... */
+    void parse_var_decl_bindings(bindings_buffer & result) {
+        parse_bindings(result, true, false);
+    }
+
+    /** \brief Parse bindings for object such as: theorems, definitions ... */
+    void parse_definition_bindings(bindings_buffer & result) {
+        parse_bindings(result, true, true);
+    }
+
     /**
         \brief Create a lambda/Pi abstraction, using the giving binders
         and body.
@@ -1859,7 +1864,7 @@ class parser::imp {
             pre_val  = parse_expr();
         } else {
             mk_scope scope(*this);
-            parse_object_bindings(bindings);
+            parse_definition_bindings(bindings);
             expr type_body;
             if (curr_is_colon()) {
                 next();
@@ -1935,7 +1940,7 @@ class parser::imp {
             type = p.first;
         } else {
             mk_scope scope(*this);
-            parse_object_bindings(bindings);
+            parse_var_decl_bindings(bindings);
             check_colon_next("invalid variable/axiom declaration, ':' expected");
             expr type_body = parse_expr();
             auto p = m_elaborator(mk_abstraction(false, bindings, type_body));
diff --git a/tests/lean/compact_def.lean b/tests/lean/compact_def.lean
new file mode 100644
index 0000000000..9d20c5fd2d
--- /dev/null
+++ b/tests/lean/compact_def.lean
@@ -0,0 +1,4 @@
+Definition f x y := x + y
+Definition g x y := sin x + y
+Definition h x y := x * sin (x + y)
+Show Environment 3
\ No newline at end of file
diff --git a/tests/lean/compact_def.lean.expected.out b/tests/lean/compact_def.lean.expected.out
new file mode 100644
index 0000000000..c2800a677d
--- /dev/null
+++ b/tests/lean/compact_def.lean.expected.out
@@ -0,0 +1,8 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Defined: f
+  Defined: g
+  Defined: h
+Definition f (x y : ℕ) : ℕ := x + y
+Definition g (x y : ℝ) : ℝ := sin x + y
+Definition h (x y : ℝ) : ℝ := x * sin (x + y)