From 5043cc75f6adc32f168b331dcd58038617e5b413 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 23 Dec 2013 13:31:55 -0800
Subject: [PATCH] fix(frontends/lean/parser): allow parenthesis in level
 expressions

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

diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 6f5eac322..63c636308 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -558,10 +558,18 @@ class parser::imp {
         return level() + val.get_unsigned_int();
     }
 
+    level parse_level_lparen() {
+        next();
+        level r = parse_level();
+        check_rparen_next("invalid level expression, ')' expected");
+        return r;
+    }
+
     level parse_level_nud() {
         switch (curr()) {
         case scanner::token::Id:        return parse_level_nud_id();
         case scanner::token::NatVal:    return parse_level_nud_int();
+        case scanner::token::LeftParen: return parse_level_lparen();
         default:
             throw parser_error("invalid level expression", pos());
         }
diff --git a/tests/lean/level1.lean b/tests/lean/level1.lean
new file mode 100644
index 000000000..7762ae223
--- /dev/null
+++ b/tests/lean/level1.lean
@@ -0,0 +1 @@
+Variable T : (Type (max U+1 U+2)).
diff --git a/tests/lean/level1.lean.expected.out b/tests/lean/level1.lean.expected.out
new file mode 100644
index 000000000..17b7357e6
--- /dev/null
+++ b/tests/lean/level1.lean.expected.out
@@ -0,0 +1,3 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Assumed: T