From 13660cfecdfb9a93a03fbb7bdb3a078992f8d21a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 16 Jan 2015 12:42:42 -0800
Subject: [PATCH] feat(frontends/lean/parser): add parse_qualified_expr

---
 src/frontends/lean/builtin_exprs.cpp | 39 +++++++++-------------------
 src/frontends/lean/parser.cpp        | 20 ++++++++++++++
 src/frontends/lean/parser.h          |  7 +++++
 3 files changed, 39 insertions(+), 27 deletions(-)

diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp
index e680972b6..2d70d74ef 100644
--- a/src/frontends/lean/builtin_exprs.cpp
+++ b/src/frontends/lean/builtin_exprs.cpp
@@ -384,51 +384,36 @@ static expr parse_ite(parser & p, expr const & c, pos_info const & pos) {
     expr t = p.parse_expr(g_then_else_prec);
     p.check_token_next(get_else_tk(), "invalid 'if-then-else' expression, 'else' expected");
     expr e = p.parse_expr(g_then_else_prec);
-    return mk_app(mk_constant(*g_ite), c, t, e);
+    return p.save_pos(mk_app(mk_constant(*g_ite), c, t, e), pos);
 }
 
-static expr parse_dite(parser & p, name const & H_name, pos_info const & pos) {
-    if (!p.env().find(*g_dite))
-        throw parser_error("invalid use of (dependent) 'if-then-else' expression, environment does "
-                           "not contain 'dite' definition", pos);
-    expr c = p.parse_expr();
+static expr parse_dite(parser & p, name const & H_name, expr const & c, pos_info const & pos) {
     p.check_token_next(get_then_tk(), "invalid 'if-then-else' expression, 'then' expected");
     expr t, e;
     {
         parser::local_scope scope(p);
         expr H = mk_local(H_name, c);
         p.add_local(H);
-        t = Fun(H, p.parse_expr(g_then_else_prec));
+        auto pos = p.pos();
+        t = p.save_pos(Fun(H, p.parse_expr(g_then_else_prec)), pos);
     }
     p.check_token_next(get_else_tk(), "invalid 'if-then-else' expression, 'else' expected");
     {
         parser::local_scope scope(p);
         expr H = mk_local(H_name, mk_app(*g_not, c));
         p.add_local(H);
-        e = Fun(H, p.parse_expr(g_then_else_prec));
+        auto pos = p.pos();
+        e = p.save_pos(Fun(H, p.parse_expr(g_then_else_prec)), pos);
     }
-    return mk_app(mk_constant(*g_dite), c, t, e);
+    return p.save_pos(mk_app(p.save_pos(mk_constant(*g_dite), pos), c, t, e), pos);
 }
 
 static expr parse_if_then_else(parser & p, unsigned, expr const *, pos_info const & pos) {
-    if (p.curr_is_identifier()) {
-        auto id_pos = p.pos();
-        name id = p.get_name_val();
-        p.next();
-        if (p.curr_is_token(get_colon_tk())) {
-            p.next();
-            return parse_dite(p, id, pos);
-        } else {
-            expr e = p.id_to_expr(id, id_pos);
-            while (!p.curr_is_token(get_then_tk())) {
-                e = p.parse_led(e);
-            }
-            return parse_ite(p, e, pos);
-        }
-    } else {
-        expr c = p.parse_expr();
-        return parse_ite(p, c, pos);
-    }
+    pair<optional<name>, expr> ie = p.parse_qualified_expr();
+    if (ie.first)
+        return parse_dite(p, *ie.first, ie.second, pos);
+    else
+        return parse_ite(p, ie.second, pos);
 }
 
 static expr parse_calc_expr(parser & p, unsigned, expr const *, pos_info const &) {
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index a85b670f4..666bce52d 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -1247,6 +1247,26 @@ expr parser::parse_expr(unsigned rbp) {
     return left;
 }
 
+pair<optional<name>, expr> parser::parse_qualified_expr(unsigned rbp) {
+    if (curr_is_identifier()) {
+        auto id_pos = pos();
+        name id = get_name_val();
+        next();
+        if (curr_is_token(get_colon_tk())) {
+            next();
+            return mk_pair(optional<name>(id), parse_expr(rbp));
+        } else {
+            expr left = id_to_expr(id, id_pos);
+            while (rbp < curr_lbp()) {
+                left = parse_led(left);
+            }
+            return mk_pair(optional<name>(), left);
+        }
+    } else {
+        return mk_pair(optional<name>(), parse_expr(rbp));
+    }
+}
+
 expr parser::parse_scoped_expr(unsigned num_ps, expr const * ps, local_environment const & lenv, unsigned rbp) {
     local_scope scope(*this);
     m_env = lenv;
diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h
index 98e221a03..866f8a074 100644
--- a/src/frontends/lean/parser.h
+++ b/src/frontends/lean/parser.h
@@ -352,6 +352,13 @@ public:
     expr id_to_expr(name const & id, pos_info const & p);
 
     expr parse_expr(unsigned rbp = 0);
+    /**
+       \brief Parse an (optionally) qualified expression.
+       If the input is of the form <id> : <expr>, then return the pair (some(id), expr).
+       Otherwise, parse the next expression and return (none, expr).
+    */
+    pair<optional<name>, expr> parse_qualified_expr(unsigned rbp = 0);
+
     expr parse_led(expr left);
     expr parse_scoped_expr(unsigned num_params, expr const * ps, local_environment const & lenv, unsigned rbp = 0);
     expr parse_scoped_expr(buffer<expr> const & ps, local_environment const & lenv, unsigned rbp = 0) {